---

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

∀e:BasicGeometry. ∀A,B,P,Q,C,D:Point.
  (C ≠ D ⇒ Colinear(C;P;Q) ⇒ Colinear(D;P;Q) ⇒ geo-tar-opp-side(e;A;B;P;Q) ⇒ geo-tar-opp-side(e;A;B;C;D))
BY
{ (Auto THEN ParallelLast THEN ExRepD THEN Auto 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-opp-side(e;A;B;P;Q)
    {}\mRightarrow{}  geo-tar-opp-side(e;A;B;C;D))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  ExRepD  THEN  Auto  THEN  EasyGeometry)

---

Home Index