---

Step * 2 1 1 1 1 of Lemma geo-le-iff


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. P : Point
6. CP ≥ AB
7. ab : {x:Point| B(OXx) ∧ Xx ≅ AB} 
8. Xab ≅ AB ∧ B(OXab)
9. cp : {x:Point| B(OXx) ∧ Xx ≅ CP} 
10. Xcp ≅ CP ∧ B(OXcp)
11. {p:Point| B(OXp)}  ⊆r Length
12. ab ∈ {p:Point| B(OXp)} 
13. cp ∈ {p:Point| B(OXp)} 
⊢ ab ∈ Length
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  P  :  Point
6.  CP  \mgeq{}  AB
7.  ab  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  AB\} 
8.  Xab  \mcong{}  AB  \mwedge{}  B(OXab)
9.  cp  :  \{x:Point|  B(OXx)  \mwedge{}  Xx  \mcong{}  CP\} 
10.  Xcp  \mcong{}  CP  \mwedge{}  B(OXcp)
11.  \{p:Point|  B(OXp)\}    \msubseteq{}r  Length
12.  ab  \mmember{}  \{p:Point|  B(OXp)\} 
13.  cp  \mmember{}  \{p:Point|  B(OXp)\} 
\mvdash{}  ab  \mmember{}  Length


By

---

Latex:
Auto

---

Home Index