---

Step * 1 1 1 1 of Lemma Euclid-erect-perp


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a ≠ b
5. c : Point
6. Colinear(a;b;c)
7. d : Point
8. Colinear(a;b;d)
9. c ≠ d
10. d' : Point
11. d_c_d'
12. dc ≅ cd'
13. d ≠ d'
14. p : Point
15. (pd' ≅ dd' ∧ pd ≅ d'd) ∧ pd ≅ pd'
16. p # d'd
17. Rpcd
18. p # cd
⊢ p ≠ c
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  a  \mneq{}  b
5.  c  :  Point
6.  Colinear(a;b;c)
7.  d  :  Point
8.  Colinear(a;b;d)
9.  c  \mneq{}  d
10.  d'  :  Point
11.  d\_c\_d'
12.  dc  \mcong{}  cd'
13.  d  \mneq{}  d'
14.  p  :  Point
15.  (pd'  \mcong{}  dd'  \mwedge{}  pd  \mcong{}  d'd)  \mwedge{}  pd  \mcong{}  pd'
16.  p  \#  d'd
17.  Rpcd
18.  p  \#  cd
\mvdash{}  p  \mneq{}  c


By

---

Latex:
Auto

---

Home Index