---

Step * of Lemma geo-out_inversion

∀e:BasicGeometry. ∀a,b,c:Point.  (out(a bc) ⇒ out(a cb))
BY
{ RepeatFor 5 ((D 0 THENA Auto))
THEN Unfold `geo-out` (-1)
THEN Unfold `geo-out` 0
THEN Auto }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (out(a  bc)  {}\mRightarrow{}  out(a  cb))


By

---

Latex:
RepeatFor  5  ((D  0  THENA  Auto))
THEN  Unfold  `geo-out`  (-1)
THEN  Unfold  `geo-out`  0
THEN  Auto

---

Home Index