---

Step * 1 1 1 1 of Lemma isosc-colinear-mid-exists


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c ≠ a
12. c ≠ a'
13. out(c bb')
14. a=m=b
15. a'c ≅ b'c
16. a' # cb'
17. x : Point
18. a'=x=b'
19. a' # cb'
20. c ≠ x
21. c ≠ m
22. a ≠ a'
23. aa' ≅ bb'
24. ¬c_x_m
25. ¬c_m_x
26. c_a_a'
⊢ False
BY
{ (((D 13 THEN ExRepD) THEN D 15) THEN (GenRepD THENA Auto) THEN (D 0 THENA Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c ≠ a
12. c ≠ a'
13. c ≠ b
14. c ≠ b'
15. a=m=b
16. a'c ≅ b'c
17. a' # cb'
18. x : Point
19. a'=x=b'
20. a' # cb'
21. c ≠ x
22. c ≠ m
23. a ≠ a'
24. aa' ≅ bb'
25. ¬c_x_m
26. ¬c_m_x
27. c_a_a'
28. c_b_b'
⊢ False

2
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c ≠ a
12. c ≠ a'
13. c ≠ b
14. c ≠ b'
15. a=m=b
16. a'c ≅ b'c
17. a' # cb'
18. x : Point
19. a'=x=b'
20. a' # cb'
21. c ≠ x
22. c ≠ m
23. a ≠ a'
24. aa' ≅ bb'
25. ¬c_x_m
26. ¬c_m_x
27. c_a_a'
28. c_b'_b
⊢ False

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  m  :  Point
6.  a'  :  Point
7.  b'  :  Point
8.  m'  :  Point
9.  c  \#  ab
10.  ac  \00D0  bc
11.  c  \mneq{}  a
12.  c  \mneq{}  a'
13.  out(c  bb')
14.  a=m=b
15.  a'c  \00D0  b'c
16.  a'  \#  cb'
17.  x  :  Point
18.  a'=x=b'
19.  a'  \#  cb'
20.  c  \mneq{}  x
21.  c  \mneq{}  m
22.  a  \mneq{}  a'
23.  aa'  \00D0  bb'
24.  \mneg{}c\_x\_m
25.  \mneg{}c\_m\_x
26.  c\_a\_a'
\mvdash{}  False


By

---

Latex:
(((D  13  THEN  ExRepD)  THEN  D  15)  THEN  (GenRepD  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index