---

Step * of Lemma geo-colinear-same

No Annotations
∀[e:BasicGeometry]. ∀[a,b:Point].  (Colinear(a;b;b) ∧ Colinear(b;a;b) ∧ Colinear(b;b;a))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. a # bb
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}[e:BasicGeometry].  \mforall{}[a,b:Point].    (Colinear(a;b;b)  \mwedge{}  Colinear(b;a;b)  \mwedge{}  Colinear(b;b;a))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index