---

Step * 1 2 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 # 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))
BY
{ ((Assert b ≡ b' BY
          (InstLemma `geo-out-unicity` [⌜e⌝;⌜c⌝;⌜b⌝;⌜b'⌝]⋅ THEN EAuto 1))
   THEN EliminatePoint' (-1)⋅
   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 # a'b'
10. a'c ≅ b'c
11. out(c a'a')
12. out(c b'b')
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. b ≡ b'
⊢ ¬((¬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  \#  a'b
10.  a'c  \00D0  bc
11.  out(c  a'a')
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  \mequiv{}  a'
\mvdash{}  \mneg{}((\mneg{}c\_x\_m)  \mwedge{}  (\mneg{}c\_m\_x))


By

---

Latex:
((Assert  b  \mequiv{}  b'  BY
                (InstLemma  `geo-out-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
  THEN  EliminatePoint'  (-1)\mcdot{}
  THEN  Auto)

---

Home Index