---

Step * of Lemma no-three-colinear-on-circle

∀[e:EuclideanPlane]. ∀[a:Point]. ∀[b:{b:Point| b ≠ a} ]. ∀[c:{c:Point| c ≠ a ∧ c ≠ b ∧ Colinear(a;b;c)} ].
  ∀p:Point. (¬(pa ≅ pb ∧ pb ≅ pc))
BY
{ (Auto THEN (D 0 THENA Auto) THEN DSetVars THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b ≠ a
5. c : Point
6. c ≠ a
7. c ≠ b
8. Colinear(a;b;c)
9. p : Point
10. pa ≅ pb
11. pb ≅ pc
⊢ False

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[a:Point].  \mforall{}[b:\{b:Point|  b  \mneq{}  a\}  ].  \mforall{}[c:\{c:Point| 
                                                                                                                          c  \mneq{}  a  \mwedge{}  c  \mneq{}  b  \mwedge{}  Colinear(a;b;c)\}  ].
    \mforall{}p:Point.  (\mneg{}(pa  \mcong{}  pb  \mwedge{}  pb  \mcong{}  pc))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  DSetVars  THEN  Auto)

---

Home Index