---

Step * of Lemma pgeo-peq-sym

∀g:ProjectivePlane. ∀a,b:Point.  (a ≡ b ⇒ b ≡ a)
BY
{ ((((Auto THEN D 0) THEN Auto) THEN D 4) THEN FLemma `pgeo-psep-sym` [4] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}a,b:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  b  \mequiv{}  a)


By

---

Latex:
((((Auto  THEN  D  0)  THEN  Auto)  THEN  D  4)  THEN  FLemma  `pgeo-psep-sym`  [4]  THEN  Auto)

---

Home Index