---

Step * of Lemma Euclid-Prop24

∀p:EuclideanPlane. ∀a,b,c,d,e,f:Point.  (a # bc ⇒ d # ef ⇒ ab ≅ de ⇒ ac ≅ df ⇒ edf < bac ⇒ bc > ef)
BY
{ (Auto THEN (InstLemma `geo-lt-angle-construction` [⌜p⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜e⌝;⌜d⌝;⌜f⌝]⋅ THENA Auto)) }

1
1. p : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a # bc
9. d # ef
10. ab ≅ de
11. ac ≅ df
12. edf < bac
13. ∃a',x',z':Point. (eda' ≅a bac ∧ x'-z'-a' ∧ out(d ex') ∧ out(d fz'))
⊢ bc > ef

---

Latex:

---

Latex:
\mforall{}p:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.
    (a  \#  bc  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  ab  \mcong{}  de  {}\mRightarrow{}  ac  \mcong{}  df  {}\mRightarrow{}  edf  <  bac  {}\mRightarrow{}  bc  >  ef)


By

---

Latex:
(Auto  THEN  (InstLemma  `geo-lt-angle-construction`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index