---

Step * of Lemma Euclid-Prop19-lemma2_1

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d,f:Point.  (a # bc ⇒ abd ≅a cbd ⇒ a=d=c ⇒ a-f-c ⇒ cbf < abf ⇒ abd < abf)
BY
{ ((Auto THEN (InstLemma `geo-lt-angle-triangle-point-exists` [⌜e⌝;⌜c⌝;⌜b⌝;⌜f⌝;⌜a⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto))
   THEN ExRepD
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜p⌝;⌜f⌝;⌜d⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. abd ≅a cbd
9. a=d=c
10. a-f-c
11. cbf < abf
12. p : Point
13. a-p-f
14. abp ≅a cbf
15. p # d
⊢ abd < abf

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. f : Point
7. a # bc
8. abd ≅a cbd
9. a=d=c
10. a-f-c
11. cbf < abf
12. p : Point
13. a-p-f
14. abp ≅a cbf
15. f # d
⊢ abd < abf

---

Latex:

---

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


By

---

Latex:
((Auto
    THEN  (InstLemma  `geo-lt-angle-triangle-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  ExRepD
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index