---

Step * 1 1 of Lemma sq_stable-geo-axioms-if


1. [g] : GeometryPrimitives
2. ∀a,b,c:Point.  SqStable(B(abc))
3. ∀a,b,c,d:Point.  SqStable(ab ≅ cd)
4. ∀a,b,c,d:Point.  SqStable(ab>cd)
5. [%6] : BasicGeometryAxioms(g)
6. ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb)))
⊢ SqStable(BasicGeometryAxioms(g))
BY
{ (Thin (-2) THEN RepUR ``basic-geo-axioms geo-eq geo-ge`` 0 THEN Auto⋅) }

1
1. [g] : GeometryPrimitives
2. ∀a,b,c:Point.  SqStable(B(abc))
3. ∀a,b,c,d:Point.  SqStable(ab ≅ cd)
4. ∀a,b,c,d:Point.  SqStable(ab>cd)
5. ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb)))
6. ∀a,b,c,d:Point.  (ab>cd ⇒ (¬cd>ab))
7. a : Point
8. b : Point
9. c : Point
10. ba>ac
⊢ SqStable(b # c)

2
1. [g] : GeometryPrimitives
2. ∀a,b,c:Point.  SqStable(B(abc))
3. ∀a,b,c,d:Point.  SqStable(ab ≅ cd)
4. ∀a,b,c,d:Point.  SqStable(ab>cd)
5. ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb)))
6. ∀a,b,c,d:Point.  (ab>cd ⇒ (¬cd>ab))
7. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
8. ∀a,b,c:Point.  (¬aa>bc)
9. ∀a,b,c,d,e,f:Point.  (ab>cd ⇒ (¬ef>cd) ⇒ ab>ef)
10. ∀a,b,c,d,e,f:Point.  ((¬cd>ab) ⇒ cd>ef ⇒ ab>ef)
11. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
12. a : Point
13. b : Point
14. c : Point
15. a leftof bc
⊢ SqStable(b leftof ca)

3
1. [g] : GeometryPrimitives
2. ∀a,b,c:Point.  SqStable(B(abc))
3. ∀a,b,c,d:Point.  SqStable(ab ≅ cd)
4. ∀a,b,c,d:Point.  SqStable(ab>cd)
5. ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb)))
6. ∀a,b,c,d:Point.  (ab>cd ⇒ (¬cd>ab))
7. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
8. ∀a,b,c:Point.  (¬aa>bc)
9. ∀a,b,c,d,e,f:Point.  (ab>cd ⇒ (¬ef>cd) ⇒ ab>ef)
10. ∀a,b,c,d,e,f:Point.  ((¬cd>ab) ⇒ cd>ef ⇒ ab>ef)
11. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
12. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
13. a : Point
14. b : Point
15. c : Point
16. a leftof bc
⊢ SqStable(b # c)

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

---

Latex:

---

Latex:

1.  [g]  :  GeometryPrimitives
2.  \mforall{}a,b,c:Point.    SqStable(B(abc))
3.  \mforall{}a,b,c,d:Point.    SqStable(ab  \mcong{}  cd)
4.  \mforall{}a,b,c,d:Point.    SqStable(ab>cd)
5.  [\%6]  :  BasicGeometryAxioms(g)
6.  \mforall{}a,b,c:Point.    (SqStable(a  \#  bc)  \mwedge{}  (a  leftof  bc  {}\mRightarrow{}  (\mneg{}a  leftof  cb)))
\mvdash{}  SqStable(BasicGeometryAxioms(g))


By

---

Latex:
(Thin  (-2)  THEN  RepUR  ``basic-geo-axioms  geo-eq  geo-ge``  0  THEN  Auto\mcdot{})

---

Home Index