---

Step * 1 1 4 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. ∀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)
BY
{ ((D 0 THENA Auto) THEN (Assert ↓z # ab BY (Unfold `geo-lsep` 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,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)
25. ↓z leftof ab
26. ↓z # ab
⊢ 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.  \mforall{}a,b,c:Point.    (SqStable(a  \#  bc)  \mwedge{}  (a  leftof  bc  {}\mRightarrow{}  (\mneg{}a  leftof  cb)))
6.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  (\mneg{}cd>ab))
7.  \mforall{}a,b,c:Point.    (ba>ac  {}\mRightarrow{}  b  \#  c)
8.  \mforall{}a,b,c:Point.    (\mneg{}aa>bc)
9.  \mforall{}a,b,c,d,e,f:Point.    (ab>cd  {}\mRightarrow{}  (\mneg{}ef>cd)  {}\mRightarrow{}  ab>ef)
10.  \mforall{}a,b,c,d,e,f:Point.    ((\mneg{}cd>ab)  {}\mRightarrow{}  cd>ef  {}\mRightarrow{}  ab>ef)
11.  \mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  ac>ab)
12.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca)
13.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \#  c)
14.  \mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))
15.  \mforall{}a,b,c,d,A,B,C,D:Point.
            (a  \#  b  {}\mRightarrow{}  B(abc)  {}\mRightarrow{}  B(ABC)  {}\mRightarrow{}  ab  \mcong{}  AB  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  ad  \mcong{}  AD  {}\mRightarrow{}  bd  \mcong{}  BD  {}\mRightarrow{}  cd  \mcong{}  CD)
16.  \mforall{}a,b,c,x,y:Point.    (ax  \mcong{}  ay  {}\mRightarrow{}  bx  \mcong{}  by  {}\mRightarrow{}  cx  \mcong{}  cy  {}\mRightarrow{}  x  \#  y  {}\mRightarrow{}  (\mneg{}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)
\mvdash{}  SqStable(z  leftof  ab)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (Assert  \mdownarrow{}z  \#  ab  BY  (Unfold  `geo-lsep`  0  THEN  Auto)))

---

Home Index