---

Step * 1 of Lemma Euclid-Prop19-lemma2


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|
BY
{ (ExRepD
   THEN (InstLemma `geo-out-interior-point-exists` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜c⌝;⌜f⌝]⋅ THEN EAuto 1)
   THEN InstLemma `geo-out-interior-point-exists` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜c⌝;⌜d⌝]⋅
   THEN EAuto 1) }

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
13. bx ≅ bc
14. out(b ax)
15. b # xc
16. ∃x':Point. (((x-x'-c ∧ out(b fx')) ∧ abf ≅a xbx') ∧ cbf ≅a cbx')
17. ∃x':Point. (((x-x'-c ∧ out(b dx')) ∧ abd ≅a xbx') ∧ cbd ≅a cbx')
⊢ |af| < |cf|

---

Latex:

---

Latex:

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  \mcong{}\msuba{}  abf
12.  \mexists{}x:Point.  ((bx  \mcong{}  bc  \mwedge{}  out(b  ax))  \mwedge{}  b  \#  xc)
\mvdash{}  |af|  <  |cf|


By

---

Latex:
(ExRepD
  THEN  (InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  InstLemma  `geo-out-interior-point-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index