---

Step * 1 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. ∀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)
BY
{ (Unfold `geo-sep` 0 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.  a  :  Point
8.  b  :  Point
9.  c  :  Point
10.  ba>ac
\mvdash{}  SqStable(b  \#  c)


By

---

Latex:
(Unfold  `geo-sep`  0  THEN  Auto)

---

Home Index