Step * of Lemma uimplies_antisymmetry

[P,Q:ℙ].  (Q supposing  supposing  uiff(P;Q))
BY
(RepeatFor ((D THENA Auto)) THEN THEN Trivial) }


Latex:


Latex:
\mforall{}[P,Q:\mBbbP{}].    (Q  supposing  P  {}\mRightarrow{}  P  supposing  Q  {}\mRightarrow{}  uiff(P;Q))


By


Latex:
(RepeatFor  4  ((D  0  THENA  Auto))  THEN  D  0  THEN  Trivial)




Home Index