---

Step * 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 # 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))
BY
{ ((((D 0 THENA Auto) THEN RepeatFor 2 (D -1))
    THEN (Assert x ≡ m BY
                InstLemma  `at-most-one-midpoint` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜x⌝;⌜m⌝]⋅)
    THEN EAuto 1)
   THEN EliminatePoint' (-1)
   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  \#  a'b'
10.  a'c  \00D0  b'c
11.  out(c  a'a')
12.  out(c  b'b')
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'
22.  b  \mequiv{}  b'
\mvdash{}  \mneg{}((\mneg{}c\_x\_m)  \mwedge{}  (\mneg{}c\_m\_x))


By

---

Latex:
((((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1))
    THEN  (Assert  x  \mequiv{}  m  BY
                            InstLemma    `at-most-one-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{})
    THEN  EAuto  1)
  THEN  EliminatePoint'  (-1)
  THEN  Auto)

---

Home Index