---

Step * of Lemma isosc-colinear-mid-exists

∀e:HeytingGeometry. ∀a,b,c,m,a',b',m':Point.
  (c # ab ⇒ ac ≅ bc ⇒ (out(c aa') ∧ out(c bb')) ⇒ a=m=b ⇒ a'c ≅ b'c ⇒ (∃m':Point. (out(c m'm) ∧ a'=m'=b')))
BY
{ ((Auto
    THEN (Assert a' # cb' BY
                (InstLemma `geo-out-triangle` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜a'⌝;⌜b'⌝]⋅ THEN Auto))
    THEN (InstLemma `isosceles-mid-exists` [⌜e⌝;⌜a'⌝;⌜c⌝;⌜b'⌝]⋅ THENA Auto))
   THEN D -1
   THEN (InstConcl [⌜x⌝]⋅ THENA Auto)
   THEN (Assert a' # cb' BY
               (InstLemma `geo-out-triangle` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜a'⌝;⌜b'⌝]⋅ THEN Auto))
   THEN (Assert c ≠ x BY
               (Unfold `geo-triangle` -1 THEN InstLemma `lsep-colinear-sep` [⌜e⌝;⌜c⌝;⌜a'⌝;⌜b'⌝;⌜x⌝]⋅ THEN Auto))
   THEN (Assert c ≠ m BY
               (InstLemma `lsep-colinear-sep` [⌜e⌝;⌜c⌝;⌜a⌝;⌜b⌝;⌜m⌝]⋅ THEN Auto))
   THEN (GenRepD ⋅ THEN D 0 THEN GenRepD)
   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
⊢ ¬((¬c_x_m) ∧ (¬c_m_x))

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,m,a',b',m':Point.
    (c  \#  ab
    {}\mRightarrow{}  ac  \00D0  bc
    {}\mRightarrow{}  (out(c  aa')  \mwedge{}  out(c  bb'))
    {}\mRightarrow{}  a=m=b
    {}\mRightarrow{}  a'c  \00D0  b'c
    {}\mRightarrow{}  (\mexists{}m':Point.  (out(c  m'm)  \mwedge{}  a'=m'=b')))


By

---

Latex:
((Auto
    THEN  (Assert  a'  \#  cb'  BY
                            (InstLemma  `geo-out-triangle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  (InstLemma  `isosceles-mid-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  D  -1
  THEN  (InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  a'  \#  cb'  BY
                          (InstLemma  `geo-out-triangle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  c  \mneq{}  x  BY
                          (Unfold  `geo-triangle`  -1
                            THEN  InstLemma  `lsep-colinear-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (Assert  c  \mneq{}  m  BY
                          (InstLemma  `lsep-colinear-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (GenRepD  \mcdot{}  THEN  D  0  THEN  GenRepD)
  THEN  Auto)

---

Home Index