Exercise:

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

© 1988-99, Carnegie Mellon University.