---

Step * of Lemma P_point-apartness-relation1

∀e:EuclideanParPlane. ∀P:P_point(e).  (¬P_point-sep(e;P;P))
BY
{ ((((Auto THEN D 0 THEN Auto) THEN Unfold `P_point-sep` -1) THEN ExRepD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}P:P\_point(e).    (\mneg{}P\_point-sep(e;P;P))


By

---

Latex:
((((Auto  THEN  D  0  THEN  Auto)  THEN  Unfold  `P\_point-sep`  -1)  THEN  ExRepD)  THEN  Auto)

---

Home Index