---

Step * 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. out(c aa')
12. out(c bb')
13. a=m=b
14. a'c ≅ b'c
15. a' # cb'
16. x : Point
17. a'=x=b'
18. a' # cb'
19. c ≠ x
20. c ≠ m
21. a ≠ a'
22. aa' ≅ bb'
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))
BY
{ ((((((D 0 THENA Auto) THEN ExRepD) THEN D 11) THEN ExRepD) THEN D 13)
   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. 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

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. 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

---

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.  out(c  aa')
12.  out(c  bb')
13.  a=m=b
14.  a'c  \00D0  b'c
15.  a'  \#  cb'
16.  x  :  Point
17.  a'=x=b'
18.  a'  \#  cb'
19.  c  \mneq{}  x
20.  c  \mneq{}  m
21.  a  \mneq{}  a'
22.  aa'  \00D0  bb'
\mvdash{}  \mneg{}((\mneg{}c\_x\_m)  \mwedge{}  (\mneg{}c\_m\_x))


By

---

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

---

Home Index