---

Step * of Lemma geo-out-strict_inversion

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

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (geo-out-strict(e;a;b;c)  {}\mRightarrow{}  geo-out-strict(e;a;c;b))


By

---

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

---

Home Index