---

Step * 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'
⊢ False
BY
{ (InstLemma `isosc-bisectors-between-ns` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜m⌝;⌜a'⌝;⌜b'⌝;⌜x⌝]⋅ 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'
\mvdash{}  False


By

---

Latex:
(InstLemma  `isosc-bisectors-between-ns`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index