---

Step * of Lemma geo-length-equality

∀e:BasicGeometry. ∀p':{p:Point| O_X_p} .  (|Xp'| = p' ∈ Length)
BY
{ (Auto THEN (EqTypeCD THEN Auto) THEN RepUR ``geo-length`` 0) }

1
1. e : BasicGeometry
2. p' : {p:Point| O_X_p} 
⊢ extend OX by Xp' ≡ p'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p':\{p:Point|  O\_X\_p\}  .    (|Xp'|  =  p')


By

---

Latex:
(Auto  THEN  (EqTypeCD  THEN  Auto)  THEN  RepUR  ``geo-length``  0)

---

Home Index