---

Step * 1 1 1 2 1 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. 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'
29. |ca'| = |ca| + |bb'| ∈ Length
30. |ca| = |ca| + |bb'| + |a'a| ∈ Length
31. |bb'| + |a'a| = 0 ∈ Length
32. |bb'| = 0 ∈ Length
⊢ False
BY
{ (FLemma `geo-zero-length-iff` [-1] THEN Auto) }

---

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.  c  \mneq{}  b
14.  c  \mneq{}  b'
15.  a=m=b
16.  a'c  \00D0  b'c
17.  a'  \#  cb'
18.  x  :  Point
19.  a'=x=b'
20.  a'  \#  cb'
21.  c  \mneq{}  x
22.  c  \mneq{}  m
23.  a  \mneq{}  a'
24.  aa'  \00D0  bb'
25.  \mneg{}c\_x\_m
26.  \mneg{}c\_m\_x
27.  c\_a'\_a
28.  c\_b\_b'
29.  |ca'|  =  |ca|  +  |bb'|
30.  |ca|  =  |ca|  +  |bb'|  +  |a'a|
31.  |bb'|  +  |a'a|  =  0
32.  |bb'|  =  0
\mvdash{}  False


By

---

Latex:
(FLemma  `geo-zero-length-iff`  [-1]  THEN  Auto)

---

Home Index