---

Step * of Lemma pgeo-psep-irrefl

∀e:ProjectivePlane. ∀[a,b:Point].  ¬a ≠ b supposing a = b ∈ Point
BY
{ ((Auto THEN Fold `pgeo-peq` 0⋅) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:ProjectivePlane.  \mforall{}[a,b:Point].    \mneg{}a  \mneq{}  b  supposing  a  =  b


By

---

Latex:
((Auto  THEN  Fold  `pgeo-peq`  0\mcdot{})  THEN  EAuto  1)

---

Home Index