---

Step * of Lemma geo-tar-same-side-invariant

∀e:BasicGeometry. ∀A,B,P,Q,C,D:Point.
  (C ≠ D ⇒ Colinear(C;P;Q) ⇒ Colinear(D;P;Q) ⇒ geo-tar-same-side(e;A;B;P;Q) ⇒ geo-tar-same-side(e;A;B;C;D))
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN D 0 THEN EasyGeometry) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,P,Q,C,D:Point.
    (C  \mneq{}  D
    {}\mRightarrow{}  Colinear(C;P;Q)
    {}\mRightarrow{}  Colinear(D;P;Q)
    {}\mRightarrow{}  geo-tar-same-side(e;A;B;P;Q)
    {}\mRightarrow{}  geo-tar-same-side(e;A;B;C;D))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  D  0  THEN  EasyGeometry)

---

Home Index