X6105 : %THEOREM%X6105 is a theorem.
FORALL n(O(OI)) .NAT n IMPLIES FORALL q(OI) .n q IMPLIES EXISTS j(I(OI)) FORALL r(OI) .r SUBSET q AND EXISTS x(I) r x IMPLIES r .j r
All rules and commands, including ADVICE, are allowed.
Only book theorems may be ASSERTed as lemmas without proof.
For a complete list of book theorems, type PROBLEMS.
This is a lemma for X6106.
You may need to ASSERT DESCR or T5310 or T5310A
TPS documentation homepage