---

Step * 2 of Lemma geo-perp-unicity


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
BY
{ PromoteHyp (-1) 5 }

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

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  u  :  Point
6.  v  :  Point
7.  a  \mneq{}  b
8.  Colinear(a;b;u)
9.  Colinear(a;b;v)
10.  ab  \mbot{}  cu
11.  ab  \mbot{}  cv
12.  \mneg{}Colinear(a;b;c)
\mvdash{}  u  \mequiv{}  v


By

---

Latex:
PromoteHyp  (-1)  5

---

Home Index