---

Step * 1 of Lemma geo-add-length_functionality


1. e : BasicGeometry
2. x : {p:Point| O_X_p} 
3. y : {p:Point| O_X_p} 
4. x' : {p:Point| O_X_p} 
5. y' : {p:Point| O_X_p} 
6. y ≡ y'
7. x ≡ x'
⊢ extend Ox by Xy ≡ extend Ox' by Xy'
BY
{ ((BLemma `geo-extend_functionality` THEN Auto) THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  \{p:Point|  O\_X\_p\} 
3.  y  :  \{p:Point|  O\_X\_p\} 
4.  x'  :  \{p:Point|  O\_X\_p\} 
5.  y'  :  \{p:Point|  O\_X\_p\} 
6.  y  \mequiv{}  y'
7.  x  \mequiv{}  x'
\mvdash{}  extend  Ox  by  Xy  \mequiv{}  extend  Ox'  by  Xy'


By

---

Latex:
((BLemma  `geo-extend\_functionality`  THEN  Auto)  THEN  RelRST  THEN  Auto)

---

Home Index