---

Step * of Lemma eu-lt-null-segment

∀e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point].  uiff(p < |aa|;False)
BY
{ ((UnivCD THENA Auto) THEN Unfold `eu-lt` 0 THEN RWO "eu-le-null-segment" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[p:\{p:Point|  O\_X\_p\}  ].  \mforall{}[a:Point].    uiff(p  <  |aa|;False)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `eu-lt`  0  THEN  RWO  "eu-le-null-segment"  0  THEN  Auto)

---

Home Index