---

Step * 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
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))
BY
{ (gSeparatedCases ⌜a⌝⌜a'⌝⋅ 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. 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'
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))

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 # a'b
10. a'c ≅ bc
11. out(c a'a')
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'
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))

---

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
\mvdash{}  \mneg{}((\mneg{}c\_x\_m)  \mwedge{}  (\mneg{}c\_m\_x))


By

---

Latex:
(gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index