X6106 : %THEOREM%

X6106 is a theorem.
Exercise:
FINITE [LAMBDA x(I) TRUTH] IMPLIES EXISTS j(I(OI)) FORALL r(OI) .EXISTS x r x IMPLIES r .j r
You may ASSERT the following theorems, without proof, as lemmas : (X6105)
You may also ASSERT any book theorem (type PROBLEMS for a list of them).
No more help available. Sorry.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage