---

Step * 1 2 of Lemma geo-add-length-between


1. e : BasicGeometry
2. a : Point
3. b : Point
4. y : {x:Point| B(OXx) ∧ Xx ≅ ab} 
5. c : Point
6. B(abc)
7. y # X
8. x : {x:Point| B(OXx) ∧ Xx ≅ ac} 
9. Xx ≅ ac
10. B(yXx)
11. Xy ≅ ab
12. B(yXy)
13. z : {x:Point| B(OXx) ∧ Xx ≅ bc} 
14. Xz ≅ bc
15. B(yXz)
16. O ≡ y
⊢ x ≡ extend Oy by Xz
BY
{ ((InstLemma `geo-between-same` [⌜e⌝;⌜y⌝;⌜X⌝]⋅ THEN Auto)
   THEN (Assert O ≡ X BY
               (RelRST THEN Auto))
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  y  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  ab\} 
5.  c  :  Point
6.  B(abc)
7.  y  \#  X
8.  x  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  ac\} 
9.  Xx  \mcong{}  ac
10.  B(yXx)
11.  Xy  \mcong{}  ab
12.  B(yXy)
13.  z  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  bc\} 
14.  Xz  \mcong{}  bc
15.  B(yXz)
16.  O  \mequiv{}  y
\mvdash{}  x  \mequiv{}  extend  Oy  by  Xz


By

---

Latex:
((InstLemma  `geo-between-same`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  O  \mequiv{}  X  BY
                          (RelRST  THEN  Auto))
  THEN  D  -1
  THEN  Auto)

---

Home Index