---

Step * of Lemma sq_stable__geo-left-axioms-1

∀g:EuclideanPlaneStructure
  (BasicGeometryAxioms(g) ⇒ (∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))) ⇒ SqStable(geo-left-axioms(g)))
BY
{ (InstLemma `sq_stable__geo-left-1` [] THEN RepeatFor 3 ((ParallelLast' THENA Auto))) }

1
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. ∀a,b,c:Point.  SqStable(a leftof bc)
⊢ SqStable(geo-left-axioms(g))

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlaneStructure
    (BasicGeometryAxioms(g)
    {}\mRightarrow{}  (\mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c))))
    {}\mRightarrow{}  SqStable(geo-left-axioms(g)))


By

---

Latex:
(InstLemma  `sq\_stable\_\_geo-left-1`  []  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto)))

---

Home Index