---

Step * 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) ∧ (BasicGeometryAxioms(g) ⇒ a leftof bc ⇒ (¬a leftof cb)))
6. ↓BasicGeometryAxioms(g)
⊢ BasicGeometryAxioms(g)
BY
{ ((Assert ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb))) BY
          (ParallelOp -2 THEN RepeatFor 3 (ParallelLast) THEN Auto))
   THEN Thin (-3)
   THEN D -2
   THEN Unhide
   THEN Try (Trivial)) }

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. [%6] : BasicGeometryAxioms(g)
6. ∀a,b,c:Point.  (SqStable(a # bc) ∧ (a leftof bc ⇒ (¬a leftof cb)))
⊢ SqStable(BasicGeometryAxioms(g))

---

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{}  (BasicGeometryAxioms(g)  {}\mRightarrow{}  a  leftof  bc  {}\mRightarrow{}  (\mneg{}a  leftof  cb)))
6.  \mdownarrow{}BasicGeometryAxioms(g)
\mvdash{}  BasicGeometryAxioms(g)


By

---

Latex:
((Assert  \mforall{}a,b,c:Point.    (SqStable(a  \#  bc)  \mwedge{}  (a  leftof  bc  {}\mRightarrow{}  (\mneg{}a  leftof  cb)))  BY
                (ParallelOp  -2  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto))
  THEN  Thin  (-3)
  THEN  D  -2
  THEN  Unhide
  THEN  Try  (Trivial))

---

Home Index