---

Step * 1 3 of Lemma geo-between-lt-angle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
8. d : Point
9. p=d=c
10. ¬out(a bc)
⊢ ∃p@0,p',x',z':Point. (bap ≅a bap@0 ∧ a_p'_p@0 ∧ (out(a bx') ∧ out(a cz')) ∧ (¬b_a_p@0) ∧ x'_p'_z' ∧ p' ≠ z')
BY
{ ((Assert a # bp BY
          (InstLemma `colinear-lsep` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜p⌝]⋅ THEN Auto))
   THEN InstConcl [⌜p⌝;⌜p⌝;⌜b⌝;⌜c⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  p  :  Point
6.  a  \#  bc
7.  b-p-c
8.  d  :  Point
9.  p=d=c
10.  \mneg{}out(a  bc)
\mvdash{}  \mexists{}p@0,p',x',z':Point
      (bap  \mcong{}\msuba{}  bap@0  \mwedge{}  a\_p'\_p@0  \mwedge{}  (out(a  bx')  \mwedge{}  out(a  cz'))  \mwedge{}  (\mneg{}b\_a\_p@0)  \mwedge{}  x'\_p'\_z'  \mwedge{}  p'  \mneq{}  z')


By

---

Latex:
((Assert  a  \#  bp  BY
                (InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index