---

Step * 1 1 1 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)
13. ab  ⊥u uc
14. ab  ⊥v vc
⊢ u ≡ v
BY
{ (RepeatFor 2 ((FLemma `geo-perp-trivial-when-colinear` [-2] THENA Auto)) THEN Auto) }

---

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.  Colinear(a;b;c)
13.  ab    \mbot{}u  uc
14.  ab    \mbot{}v  vc
\mvdash{}  u  \mequiv{}  v


By

---

Latex:
(RepeatFor  2  ((FLemma  `geo-perp-trivial-when-colinear`  [-2]  THENA  Auto))  THEN  Auto)

---

Home Index