---

Step * 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'
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))
BY
{ (Assert aa' ≅ bb' BY
         (InstLemma `geo-out-cong-cong` [⌜e⌝;⌜c⌝;⌜a⌝;⌜a'⌝;⌜c⌝;⌜b⌝;⌜b'⌝]⋅ THEN 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'
22. aa' ≅ bb'
⊢ ¬((¬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
21.  a  \mneq{}  a'
\mvdash{}  \mneg{}((\mneg{}c\_x\_m)  \mwedge{}  (\mneg{}c\_m\_x))


By

---

Latex:
(Assert  aa'  \00D0  bb'  BY
              (InstLemma  `geo-out-cong-cong`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index