X6106 : %THEOREM%X6106 is a theorem.
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