T5310 : %THEOREM%

T5310 is a theorem.
Book Theorem:
FORALL z(A) [p(OA) z EQUIV y(A) = z] IMPLIES IOTA p = y
Theorem about descriptions.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage