---

Step * of Lemma basic-geo-axioms-imply

No Annotations
∀g:EuclideanPlaneStructure
  (BasicGeometryAxioms(g) ⇒ ((∀a:Point. a ≡ a) ∧ (∀a,b:Point.  ab ≅ ba) ∧ (∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D -1 THEN SplitAndHyps THEN Auto) }

1
1. g : 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,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
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. a : Point
⊢ a ≡ a

2
1. g : 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,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
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. ∀a:Point. a ≡ a
16. a : Point
17. b : Point
⊢ ab ≅ ba

3
1. g : 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,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
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. ∀a:Point. a ≡ a
16. ∀a,b:Point.  ab ≅ ba
17. a : Point
18. b : Point
19. c : Point
20. a ≡ b
⊢ ac ≅ bc

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlaneStructure
    (BasicGeometryAxioms(g)
    {}\mRightarrow{}  ((\mforall{}a:Point.  a  \mequiv{}  a)  \mwedge{}  (\mforall{}a,b:Point.    ab  \mcong{}  ba)  \mwedge{}  (\mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  -1  THEN  SplitAndHyps  THEN  Auto)

---

Home Index