---

Step * of Lemma basic-geo-sep-sym

No Annotations
∀e:GeometryPrimitives. (BasicGeometryAxioms(e) ⇒ (∀a,b:Point.  (a # b ⇒ b # a)))
BY
{ (Auto
   THEN (Assert ∀a,b,c,d,x,y:Point.  (ab ≅ cd ⇒ cd>xy ⇒ ab>xy) BY
               (InstLemma `basic-geo-cong-preserves-gt-prim` [⌜e⌝]⋅ THEN Auto))
   THEN (Assert ∀a:Point. (¬a # a) BY
               (InstLemma `geo-sep-irreflexive` [⌜e⌝]⋅ THEN Auto))
   THEN (Assert ∀a,b:Point.  ba ≥ ab BY
               ((Unfold `geo-ge` 0 THEN Auto) THEN InstLemma `geo-gt-prim-irreflexive` [⌜e⌝;⌜a1⌝;⌜b1⌝]⋅ THEN Auto))) }

1
1. e : GeometryPrimitives
2. BasicGeometryAxioms(e)
3. a : Point
4. b : Point
5. a # b
6. ∀a,b,c,d,x,y:Point.  (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
7. ∀a:Point. (¬a # a)
8. ∀a,b:Point.  ba ≥ ab
⊢ b # a

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:GeometryPrimitives.  (BasicGeometryAxioms(e)  {}\mRightarrow{}  (\mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}a,b,c,d,x,y:Point.    (ab  \mcong{}  cd  {}\mRightarrow{}  cd>xy  {}\mRightarrow{}  ab>xy)  BY
                          (InstLemma  `basic-geo-cong-preserves-gt-prim`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}a:Point.  (\mneg{}a  \#  a)  BY
                          (InstLemma  `geo-sep-irreflexive`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}a,b:Point.    ba  \mgeq{}  ab  BY
                          ((Unfold  `geo-ge`  0  THEN  Auto)
                            THEN  InstLemma  `geo-gt-prim-irreflexive`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
                            THEN  Auto)))

---

Home Index