---

Step * 1 1 1 2 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'
⊢ False
BY
{ ((FLemma `geo-add-length-between` [-1] THENA Auto) THEN (FLemma `geo-add-length-between` [-3] 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'
29. |cb'| = |cb| + |bb'| ∈ Length
30. |ca| = |ca'| + |a'a| ∈ Length
⊢ 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.  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'
\mvdash{}  False


By

---

Latex:
((FLemma  `geo-add-length-between`  [-1]  THENA  Auto)
  THEN  (FLemma  `geo-add-length-between`  [-3]  THENA  Auto)
  )

---

Home Index