---

Step * of Lemma uimplies_antisymmetry

∀[P,Q:ℙ].  (Q supposing P ⇒ P supposing Q ⇒ uiff(P;Q))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN D 0 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