---

Step * of Lemma geo-colinear-preserves-parallel2

∀e:EuclideanPlane. ∀a,b,c,d,x,y:Point.
  (geo-parallel-points(e;a;b;c;d)
  ⇒ Colinear(a;b;x)
  ⇒ Colinear(c;d;y)
  ⇒ c ≠ y
  ⇒ a ≠ x
  ⇒ geo-parallel-points(e;a;x;c;y))
BY
{ (Auto
   THEN (InstLemma `geo-colinear-preserves-parallel` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜x⌝]⋅ THEN Auto)
   THEN (FLemma `geo-parallel-points-symmetry` [-1] THEN Auto)
   THEN (InstLemma `geo-colinear-preserves-parallel` [⌜e⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜x⌝;⌜y⌝]⋅ THEN Auto)
   THEN FLemma `geo-parallel-points-symmetry` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,x,y:Point.
    (geo-parallel-points(e;a;b;c;d)
    {}\mRightarrow{}  Colinear(a;b;x)
    {}\mRightarrow{}  Colinear(c;d;y)
    {}\mRightarrow{}  c  \mneq{}  y
    {}\mRightarrow{}  a  \mneq{}  x
    {}\mRightarrow{}  geo-parallel-points(e;a;x;c;y))


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-colinear-preserves-parallel`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (FLemma  `geo-parallel-points-symmetry`  [-1]  THEN  Auto)
  THEN  (InstLemma  `geo-colinear-preserves-parallel`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  FLemma  `geo-parallel-points-symmetry`  [-1]
  THEN  Auto)

---

Home Index