---

Step * 1 1 2 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. ∀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
16. ↓b leftof ca
17. ↓b # ca
⊢ b leftof ca
BY
{ (((Assert b # ca BY Auto) THEN D -1 THEN Auto)
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN InstHyp [⌜b⌝;⌜a⌝;⌜c⌝] (5)⋅
   THEN Auto) }

---

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.  a  :  Point
13.  b  :  Point
14.  c  :  Point
15.  a  leftof  bc
16.  \mdownarrow{}b  leftof  ca
17.  \mdownarrow{}b  \#  ca
\mvdash{}  b  leftof  ca


By

---

Latex:
(((Assert  b  \#  ca  BY  Auto)  THEN  D  -1  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (5)\mcdot{}
  THEN  Auto)

---

Home Index