---

Step * 1 of Lemma sq_stable__geo-axioms


1. g : EuclideanPlaneStructure
2. a : Point
3. b : Point
4. c : Point
5. SqStable(a # bc)
6. BasicGeometryAxioms(g)
7. a leftof bc
⊢ ¬a leftof cb
BY
{ (FLemma `basic-geo-not-left-and-right` [-1]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlaneStructure
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  SqStable(a  \#  bc)
6.  BasicGeometryAxioms(g)
7.  a  leftof  bc
\mvdash{}  \mneg{}a  leftof  cb


By

---

Latex:
(FLemma  `basic-geo-not-left-and-right`  [-1]\mcdot{}  THEN  Auto)

---

Home Index