---

Step * 2 1 1 of Lemma geo-perp-unicity


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
13. c ≠ u
14. c ≠ v
15. Rcuv
16. Rcvu
⊢ u ≡ v
BY
{ (FLemma `right-angles-not-complementary` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(FLemma  `right-angles-not-complementary`  [-1;-2]  THEN  Auto)

---

Home Index