---

Step * of Lemma geo-out-to-bet

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.  (Colinear(a';b';c') ⇒ (out(b ac) ⇐⇒ out(b' a'c')) ⇒ a_b_c ⇒ a'_b'_c')
BY
{ (Auto THEN (FLemma `geo-not-bet-and-out` [-1] THENA Auto) THEN BLemma `geo-colinear-not-out` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',b',c':Point.
    (Colinear(a';b';c')  {}\mRightarrow{}  (out(b  ac)  \mLeftarrow{}{}\mRightarrow{}  out(b'  a'c'))  {}\mRightarrow{}  a\_b\_c  {}\mRightarrow{}  a'\_b'\_c')


By

---

Latex:
(Auto
  THEN  (FLemma  `geo-not-bet-and-out`  [-1]  THENA  Auto)
  THEN  BLemma  `geo-colinear-not-out`
  THEN  Auto)

---

Home Index