---

Step * of Lemma geo-perp-unicity

∀e:BasicGeometry. ∀a,b,c,u,v:Point.  (a ≠ b ⇒ Colinear(a;b;u) ⇒ Colinear(a;b;v) ⇒ ab ⊥ cu ⇒ ab ⊥ cv ⇒ u ≡ v)
BY
{ (Auto THEN (StableCases ⌜Colinear(a;b;c)⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. u : Point
6. v : Point
7. a ≠ b
8. Colinear(a;b;u)
9. Colinear(a;b;v)
10. ab ⊥ cu
11. ab ⊥ cv
12. Colinear(a;b;c)
⊢ u ≡ v

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. u : Point
6. v : Point
7. a ≠ b
8. Colinear(a;b;u)
9. Colinear(a;b;v)
10. ab ⊥ cu
11. ab ⊥ cv
12. ¬Colinear(a;b;c)
⊢ u ≡ v

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,u,v:Point.
    (a  \mneq{}  b  {}\mRightarrow{}  Colinear(a;b;u)  {}\mRightarrow{}  Colinear(a;b;v)  {}\mRightarrow{}  ab  \mbot{}  cu  {}\mRightarrow{}  ab  \mbot{}  cv  {}\mRightarrow{}  u  \mequiv{}  v)


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}Colinear(a;b;c)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index