---

Step * of Lemma Euclid-Prop18-lemma

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (a # bc ⇒ b-c-d ⇒ bac < bad)
BY
{ (Auto
   THEN ((Assert a ≠ d BY
                ((InstLemma `sep-if-all-lsep` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝] ⋅ THENA Auto) THEN InstHyp [⌜d⌝] (-1)⋅ THEN Auto))
         THEN (Assert ¬out(a bd) BY
                     ((Assert a # bd BY Auto) THEN (D 0 THENA Auto) THEN FLemma `not-lsep-if-out` [-1]⋅ THEN Auto))
         )
   THEN Unfold `geo-lt-angle` 0
   THEN GenRepD) }

1
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')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (a  \#  bc  {}\mRightarrow{}  b-c-d  {}\mRightarrow{}  bac  <  bad)


By

---

Latex:
(Auto
  THEN  ((Assert  a  \mneq{}  d  BY
                            ((InstLemma  `sep-if-all-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  \mcdot{}  THENA  Auto)
                              THEN  InstHyp  [\mkleeneopen{}d\mkleeneclose{}]  (-1)\mcdot{}
                              THEN  Auto))
              THEN  (Assert  \mneg{}out(a  bd)  BY
                                      ((Assert  a  \#  bd  BY
                                                      Auto)
                                        THEN  (D  0  THENA  Auto)
                                        THEN  FLemma  `not-lsep-if-out`  [-1]\mcdot{}
                                        THEN  Auto))
              )
  THEN  Unfold  `geo-lt-angle`  0
  THEN  GenRepD)

---

Home Index