---

Step * 2 1 1 1 2 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)} 
14. ¬B(Xabcp)
⊢ False
BY
{ ((InstLemma `geo-between-same-side2` [⌜e⌝;⌜O⌝;⌜X⌝;⌜ab⌝;⌜cp⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepeatFor 2 ((D 0 THENA 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)} 
14. ¬B(Xabcp)
15. B(Xabcp)
⊢ False

2
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)} 
14. ¬B(Xabcp)
15. B(Xcpab)
⊢ False

---

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)\} 
14.  \mneg{}B(Xabcp)
\mvdash{}  False


By

---

Latex:
((InstLemma  `geo-between-same-side2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}ab\mkleeneclose{};\mkleeneopen{}cp\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index