X6201 : %THEOREM%X6201 is a theorem.
EXISTS r(OAA) FORALL x(A) FORALL y(A) FORALL z(A) [EXISTS w(A) r x w AND ~r x x AND .r x y IMPLIES .r y z IMPLIES r x z] IMPLIES EXISTS R(O(OA)(OA)) FORALL X(OA) FORALL Y(OA) FORALL Z(OA) .EXISTS W(OA) R X W AND ~R X X AND .R X Y IMPLIES .R Y Z IMPLIES R X Z
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.
No more help available. Sorry.
TPS documentation homepage