---

Step * of Lemma Euclid-Prop19-lemma2

∀e:EuclideanPlane. ∀a,b,c,d,f:Point.  (a # bc ⇒ cbd < abd ⇒ a=d=c ⇒ a-f-c ⇒ cbf ≅a abf ⇒ |af| < |cf|)
BY
{ (Auto THEN InstLemma `geo-equilateral-exists` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝]⋅ THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. cbd < abd
9. a=d=c
10. a-f-c
11. cbf ≅a abf
12. ∃x:Point. ((bx ≅ bc ∧ out(b ax)) ∧ b # xc)
⊢ |af| < |cf|

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,f:Point.
    (a  \#  bc  {}\mRightarrow{}  cbd  <  abd  {}\mRightarrow{}  a=d=c  {}\mRightarrow{}  a-f-c  {}\mRightarrow{}  cbf  \mcong{}\msuba{}  abf  {}\mRightarrow{}  |af|  <  |cf|)


By

---

Latex:
(Auto  THEN  InstLemma  `geo-equilateral-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index