---

Step * of Lemma angle-bisector-unique

∀e:EuclideanPlane. ∀a,b,c,a',c',x,y:Point.
  (a # bc ⇒ out(b aa') ⇒ out(b cc') ⇒ a-x-c ⇒ a'-y-c' ⇒ abx ≅a cbx ⇒ a'by ≅a c'by ⇒ {out(b xy) ∧ abx ≅a a'by})
BY
{ ((Auto
    THEN ((InstLemma `geo-out-interior-point-exists` [⌜e⌝;⌜a'⌝;⌜b⌝;⌜c'⌝;⌜a⌝;⌜c⌝;⌜y⌝]⋅ THENA EAuto 1)
          THENA (InstLemma `out-preserves-lsep` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜a'⌝;⌜c'⌝]⋅ THEN EAuto 1)
          )
    )
   THEN (ExRepD THEN (gProperProlong ⌜c⌝⌜b⌝`C'⌜O⌝⌜X⌝⋅ THENA Auto) THEN (gProperProlong ⌜C⌝⌜b⌝`c\'\''⌜b⌝⌜a⌝⋅ THENA Auto))
   THEN (Assert out(b cc'') BY
               ((InstLemma `geo-out-iff-between1` [⌜e⌝;⌜b⌝;⌜c⌝;⌜c''⌝;⌜C⌝]⋅ THEN Auto) THEN D -2))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. y : Point
9. a # bc
10. out(b aa')
11. out(b cc')
12. a-x-c
13. a'-y-c'
14. abx ≅a cbx
15. a'by ≅a c'by
16. x' : Point
17. a-x'-c
18. out(b yx')
19. a'by ≅a abx'
20. c'by ≅a cbx'
21. C : Point
22. c-b-C ∧ bC ≅ OX
23. c'' : Point
24. C-b-c'' ∧ bc'' ≅ ba
25. out(b cc'')
⊢ out(b xy) ∧ abx ≅a a'by

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',c',x,y:Point.
    (a  \#  bc
    {}\mRightarrow{}  out(b  aa')
    {}\mRightarrow{}  out(b  cc')
    {}\mRightarrow{}  a-x-c
    {}\mRightarrow{}  a'-y-c'
    {}\mRightarrow{}  abx  \mcong{}\msuba{}  cbx
    {}\mRightarrow{}  a'by  \mcong{}\msuba{}  c'by
    {}\mRightarrow{}  \{out(b  xy)  \mwedge{}  abx  \mcong{}\msuba{}  a'by\})


By

---

Latex:
((Auto
    THEN  ((InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
                THENA  (InstLemma  `out-preserves-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
                )
    )
  THEN  (ExRepD
              THEN  (gProperProlong  \mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`C'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProperProlong  \mkleeneopen{}C\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`c\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (Assert  out(b  cc'')  BY
                          ((InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -2)))

---

Home Index