---

Step * of Lemma sq_stable__geo-left-axioms

∀g:EuclideanPlane
  SqStable((∀a,b,c:Point.  (¬a # bc ⇐⇒ Colinear(a;b;c)))
  ∧ (∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca))
  ∧ (∀a,b,c:Point.  (a leftof bc ⇒ b # c))
  ∧ (∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z # ab))
  ∧ (∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ Colinear(y;a;b) ⇒ y # bc)))
BY
{ (Auto THEN BLemma `sq_stable-geo-axioms-if` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane
    SqStable((\mforall{}a,b,c:Point.    (\mneg{}a  \#  bc  \mLeftarrow{}{}\mRightarrow{}  Colinear(a;b;c)))
    \mwedge{}  (\mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca))
    \mwedge{}  (\mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \#  c))
    \mwedge{}  (\mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  \#  ab))
    \mwedge{}  (\mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \#  b  {}\mRightarrow{}  Colinear(y;a;b)  {}\mRightarrow{}  y  \#  bc)))


By

---

Latex:
(Auto  THEN  BLemma  `sq\_stable-geo-axioms-if`  THEN  Auto)

---

Home Index