---

Step * of Lemma circle-not-colinear

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab ≅ ac ⇒ ab ≅ ad ⇒ b ≠ c ⇒ c ≠ d ⇒ d ≠ b ⇒ (¬Colinear(b;c;d)))
BY
{ (Auto THEN (D 0 THENA Auto) THEN InstLemma `no-three-colinear-on-circle` [⌜e⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (ab  \mcong{}  ac  {}\mRightarrow{}  ab  \mcong{}  ad  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  c  \mneq{}  d  {}\mRightarrow{}  d  \mneq{}  b  {}\mRightarrow{}  (\mneg{}Colinear(b;c;d)))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  InstLemma  `no-three-colinear-on-circle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index