---

Step * 2 1 1 1 of Lemma geo-sep-irrefl_gt-prim

.....aux..... 
1. e : EuclideanPlane
2. c : Point
3. a : Point
4. b : Point
5. b ≡ c
6. aa>cc
⊢ cc ≅ aa
BY
{ (UseGeoAxioms THEN InstHyp [⌜a⌝;⌜a⌝;⌜c⌝] (7)⋅ THEN Auto) }

1
1. e : EuclideanPlane
2. c : Point
3. a : Point
4. b : Point
5. b ≡ c
6. aa>cc
7. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
8. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
9. ∀a,b,c:Point.  bc ≥ aa
10. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
11. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
12. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
13. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
14. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
15. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
16. ∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
17. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
18. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
19. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
20. ∀d:Point. (aa>cd ⇒ aa ≥ cd)
⊢ cc ≅ aa

---

Latex:

---

Latex:
.....aux..... 
1.  e  :  EuclideanPlane
2.  c  :  Point
3.  a  :  Point
4.  b  :  Point
5.  b  \mequiv{}  c
6.  aa>cc
\mvdash{}  cc  \mcong{}  aa


By

---

Latex:
(UseGeoAxioms  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (7)\mcdot{}  THEN  Auto)

---

Home Index