---

Step * of Lemma sq_stable-geo-axioms-if

No Annotations
∀[g:GeometryPrimitives]
  ((∀a,b,c:Point.  SqStable(B(abc)))
  ⇒ (∀a,b,c,d:Point.  SqStable(ab ≅ cd))
  ⇒ (∀a,b,c,d:Point.  SqStable(ab>cd))
  ⇒ (∀a,b,c:Point.  (SqStable(a # bc) ∧ (BasicGeometryAxioms(g) ⇒ a leftof bc ⇒ (¬a leftof cb))))
  ⇒ SqStable(BasicGeometryAxioms(g)))
BY
{ ((UnivCD THENA Auto⋅) THEN (D 0 THENA 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) ∧ (BasicGeometryAxioms(g) ⇒ a leftof bc ⇒ (¬a leftof cb)))
6. ↓BasicGeometryAxioms(g)
⊢ BasicGeometryAxioms(g)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:GeometryPrimitives]
    ((\mforall{}a,b,c:Point.    SqStable(B(abc)))
    {}\mRightarrow{}  (\mforall{}a,b,c,d:Point.    SqStable(ab  \mcong{}  cd))
    {}\mRightarrow{}  (\mforall{}a,b,c,d:Point.    SqStable(ab>cd))
    {}\mRightarrow{}  (\mforall{}a,b,c:Point.    (SqStable(a  \#  bc)  \mwedge{}  (BasicGeometryAxioms(g)  {}\mRightarrow{}  a  leftof  bc  {}\mRightarrow{}  (\mneg{}a  leftof  cb))))
    {}\mRightarrow{}  SqStable(BasicGeometryAxioms(g)))


By

---

Latex:
((UnivCD  THENA  Auto\mcdot{})  THEN  (D  0  THENA  Auto))

---

Home Index