---

Step * of Lemma geo-perp-trivial-when-colinear

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (b ≠ a ⇒ Colinear(a;b;c) ⇒ ab  ⊥d dc ⇒ d ≡ c)
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b ≠ a
7. Colinear(a;b;c)
8. ab  ⊥d dc
9. d ≠ c
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (b  \mneq{}  a  {}\mRightarrow{}  Colinear(a;b;c)  {}\mRightarrow{}  ab    \mbot{}d  dc  {}\mRightarrow{}  d  \mequiv{}  c)


By

---

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

---

Home Index