---

Step * 1 of Lemma euclidean-plane-axioms


1. g : EuclideanPlane
2. BasicGeometryAxioms(g) ∧ (∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c))))
⊢ ((∀a,b:Point.  (a # b ⇒ b # a))
  ∧ (∀a:Point. (¬a # a))
  ∧ (∀a,b,x,y:Point.  (a ≡ b ⇒ B(xay) ⇒ B(xby)))
  ∧ ((∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ cb)) ∧ (∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)))
  ∧ (∀a,b,c,d:Point.  (cd ≥ ab ⇒ a # b ⇒ c # d))
  ∧ (∀a,b,c:Point.  (a ≡ b ⇒ B(abc)))
  ∧ (∀a,b,c:Point.  (B(abc) ⇒ B(cba)))
  ∧ (∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc)))
  ∧ (∀a,b:Point.  ab ≅ ba)
  ∧ (∀a,b,p,q,r,s:Point.  (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
  ∧ (∀a,b:Point.  aa ≅ bb)
  ∧ (∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)))
∧ (∀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
{ ((InstLemma `sq_stable__geo-left-axioms-1` [⌜g⌝]⋅ THENA Auto)
   THEN (InstLemma `basic-geo-axioms-imply` [⌜g⌝]⋅ THENA Auto)
   THEN (InstLemma `basic-geo-sep-sym` [⌜g⌝]⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. BasicGeometryAxioms(g) ∧ (∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c))))
3. SqStable(geo-left-axioms(g))
4. (∀a:Point. a ≡ a) ∧ (∀a,b:Point.  ab ≅ ba) ∧ (∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc))
5. ∀a,b:Point.  (a # b ⇒ b # a)
⊢ ((∀a,b:Point.  (a # b ⇒ b # a))
  ∧ (∀a:Point. (¬a # a))
  ∧ (∀a,b,x,y:Point.  (a ≡ b ⇒ B(xay) ⇒ B(xby)))
  ∧ ((∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ cb)) ∧ (∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)))
  ∧ (∀a,b,c,d:Point.  (cd ≥ ab ⇒ a # b ⇒ c # d))
  ∧ (∀a,b,c:Point.  (a ≡ b ⇒ B(abc)))
  ∧ (∀a,b,c:Point.  (B(abc) ⇒ B(cba)))
  ∧ (∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc)))
  ∧ (∀a,b:Point.  ab ≅ ba)
  ∧ (∀a,b,p,q,r,s:Point.  (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
  ∧ (∀a,b:Point.  aa ≅ bb)
  ∧ (∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)))
∧ (∀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))

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  BasicGeometryAxioms(g)  \mwedge{}  (\mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c))))
\mvdash{}  ((\mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a))
    \mwedge{}  (\mforall{}a:Point.  (\mneg{}a  \#  a))
    \mwedge{}  (\mforall{}a,b,x,y:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  B(xay)  {}\mRightarrow{}  B(xby)))
    \mwedge{}  ((\mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  cb))  \mwedge{}  (\mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)))
    \mwedge{}  (\mforall{}a,b,c,d:Point.    (cd  \mgeq{}  ab  {}\mRightarrow{}  a  \#  b  {}\mRightarrow{}  c  \#  d))
    \mwedge{}  (\mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  B(abc)))
    \mwedge{}  (\mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  B(cba)))
    \mwedge{}  (\mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc)))
    \mwedge{}  (\mforall{}a,b:Point.    ab  \mcong{}  ba)
    \mwedge{}  (\mforall{}a,b,p,q,r,s:Point.    (ab  \mcong{}  pq  {}\mRightarrow{}  ab  \mcong{}  rs  {}\mRightarrow{}  pq  \mcong{}  rs))
    \mwedge{}  (\mforall{}a,b:Point.    aa  \mcong{}  bb)
    \mwedge{}  (\mforall{}a,b,c,d,A,B,C,D:Point.
              (a  \#  b  {}\mRightarrow{}  B(abc)  {}\mRightarrow{}  B(ABC)  {}\mRightarrow{}  ab  \mcong{}  AB  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  ad  \mcong{}  AD  {}\mRightarrow{}  bd  \mcong{}  BD  {}\mRightarrow{}  cd  \mcong{}  CD)))
\mwedge{}  (\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:
((InstLemma  `sq\_stable\_\_geo-left-axioms-1`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `basic-geo-axioms-imply`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `basic-geo-sep-sym`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index