---

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


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. ¬((¬a_c_b) ∧ (¬a_b_c))
8. d : Point
9. b_a_d
10. ba ≅ ad
11. d_a_c
12. c ≠ d
13. d' : Point
14. d_c_d'
15. dc ≅ cd'
16. out(b ad)
17. out(d bd')
18. d ≠ c
19. d_c_d'
20. dc ≅ cd'
21. Colinear(a;b;d)
22. x : Point
23. x leftof dd'
⊢ ¬((¬d'_d_a) ∧ (¬d'_a_d))
BY
{ ((D 0 THENA Auto) THEN D 7 THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. d : Point
8. b_a_d
9. ba ≅ ad
10. d_a_c
11. c ≠ d
12. d' : Point
13. d_c_d'
14. dc ≅ cd'
15. out(b ad)
16. out(d bd')
17. d ≠ c
18. d_c_d'
19. dc ≅ cd'
20. Colinear(a;b;d)
21. x : Point
22. x leftof dd'
23. (¬d'_d_a) ∧ (¬d'_a_d)
24. a_c_b
⊢ False

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. Colinear(a;b;c)
7. d : Point
8. b_a_d
9. ba ≅ ad
10. d_a_c
11. c ≠ d
12. d' : Point
13. d_c_d'
14. dc ≅ cd'
15. out(b ad)
16. out(d bd')
17. d ≠ c
18. d_c_d'
19. dc ≅ cd'
20. Colinear(a;b;d)
21. x : Point
22. x leftof dd'
23. (¬d'_d_a) ∧ (¬d'_a_d)
24. a_b_c
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \mneq{}  b
6.  Colinear(a;b;c)
7.  \mneg{}((\mneg{}a\_c\_b)  \mwedge{}  (\mneg{}a\_b\_c))
8.  d  :  Point
9.  b\_a\_d
10.  ba  \mcong{}  ad
11.  d\_a\_c
12.  c  \mneq{}  d
13.  d'  :  Point
14.  d\_c\_d'
15.  dc  \mcong{}  cd'
16.  out(b  ad)
17.  out(d  bd')
18.  d  \mneq{}  c
19.  d\_c\_d'
20.  dc  \mcong{}  cd'
21.  Colinear(a;b;d)
22.  x  :  Point
23.  x  leftof  dd'
\mvdash{}  \mneg{}((\mneg{}d'\_d\_a)  \mwedge{}  (\mneg{}d'\_a\_d))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  7  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index