---

Step * 1 of Lemma Euclid-Prop18-lemma


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. a ≠ d
9. ¬out(a bd)
⊢ ∃p,p',x',z':Point. (bac ≅a bap ∧ a_p'_p ∧ (out(a bx') ∧ out(a dz')) ∧ (¬b_a_p) ∧ x'_p'_z' ∧ p' ≠ z')
BY
{ (InstConcl [⌜c⌝;⌜c⌝;⌜b⌝;⌜d⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstConcl  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index