---

Step * of Lemma geo-add-length-property3

No Annotations
∀g:EuclideanPlane. ∀p,q:{p:Point| B(OXp)} .  (B(Xpq) ⇒ p + |pq| ≡ q)
BY
{ Auto }

1
1. g : EuclideanPlane
2. p : {p:Point| B(OXp)} 
3. q : {p:Point| B(OXp)} 
4. B(Xpq)
⊢ p + |pq| ≡ q

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}p,q:\{p:Point|  B(OXp)\}  .    (B(Xpq)  {}\mRightarrow{}  p  +  |pq|  \mequiv{}  q)


By

---

Latex:
Auto

---

Home Index