---

Step * of Lemma isosc-bisectors-between

∀e:HeytingGeometry. ∀a,b,c,m,a',b',m':Point.
  (c # ab ⇒ ac ≅ bc ⇒ (c-a-a' ∧ b'-b-c) ⇒ a=m=b ⇒ a'=m'=b' ⇒ aa' ≅ bb' ⇒ c-m-m')
BY
{ (Auto
   THEN (Assert a' # b'c BY
               (InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜a'⌝]⋅ THEN Auto))
   THEN (Assert c ≠ m' BY
               (InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜c⌝;⌜m'⌝]⋅
                THEN Auto
                THEN FLemma `midpoint-sep` [14]
                THEN Auto
                THEN D 14
                THEN Auto))
   THEN (Assert c ≠ m BY
               (InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜m⌝]⋅
                THEN Auto
                THEN FLemma `midpoint-sep` [13]
                THEN Auto
                THEN D 13
                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. c-a-a'
12. b'-b-c
13. a=m=b
14. a'=m'=b'
15. aa' ≅ bb'
16. a' # b'c
17. c ≠ m'
18. c ≠ m
⊢ c-m-m'

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  a'  \#  b'c  BY
                          (InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  c  \mneq{}  m'  BY
                          (InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}m'\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  FLemma  `midpoint-sep`  [14]
                            THEN  Auto
                            THEN  D  14
                            THEN  Auto))
  THEN  (Assert  c  \mneq{}  m  BY
                          (InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  FLemma  `midpoint-sep`  [13]
                            THEN  Auto
                            THEN  D  13
                            THEN  Auto)))

---

Home Index