---

Step * 2 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)} 
⊢ ∃p',q':{p:Point| B(OXp)} . ((p' = ab ∈ Length) ∧ (q' = cp ∈ Length) ∧ B(Xp'q'))
BY
{ (InstConcl [⌜ab⌝;⌜cp⌝]⋅ THENW Auto) }

1
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 = ab ∈ Length) ∧ (cp = cp ∈ Length) ∧ B(Xabcp)

---

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{}  \mexists{}p',q':\{p:Point|  B(OXp)\}  .  ((p'  =  ab)  \mwedge{}  (q'  =  cp)  \mwedge{}  B(Xp'q'))


By

---

Latex:
(InstConcl  [\mkleeneopen{}ab\mkleeneclose{};\mkleeneopen{}cp\mkleeneclose{}]\mcdot{}  THENW  Auto)

---

Home Index