---

Step * of Lemma basic-axioms-imply_between1

No Annotations
∀e:EuclideanPlaneStructure. (BasicGeometryAxioms(e) ⇒ (∀a1,a2,b,c:Point.  (a1 ≡ a2 ⇒ B(a1bc) ⇒ B(a2bc))))
BY
{ (Auto
   THEN (InstLemma `basic-geo-axioms-imply` [⌜e⌝]⋅ THENA Auto)
   THEN (InstLemma `basic-geo-sep-sym` [⌜e⌝]⋅ THENA Auto)
   THEN D 2
   THEN ExRepD) }

1
1. e : EuclideanPlaneStructure
2. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
3. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
4. ∀a,b,c:Point.  bc ≥ aa
5. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
7. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
8. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
9. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
10. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
11. ∀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)
12. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
13. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
14. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
15. a1 : Point
16. a2 : Point
17. b : Point
18. c : Point
19. a1 ≡ a2
20. B(a1bc)
21. ∀a:Point. a ≡ a
22. ∀a,b:Point.  ab ≅ ba
23. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
24. ∀a,b:Point.  (a # b ⇒ b # a)
⊢ B(a2bc)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlaneStructure
    (BasicGeometryAxioms(e)  {}\mRightarrow{}  (\mforall{}a1,a2,b,c:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  B(a1bc)  {}\mRightarrow{}  B(a2bc))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `basic-geo-axioms-imply`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `basic-geo-sep-sym`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  2
  THEN  ExRepD)

---

Home Index