---

Step * of Lemma geo-gt-prim-irreflexive

No Annotations
∀e:GeometryPrimitives. (BasicGeometryAxioms(e) ⇒ (∀a,b:Point.  (¬ab>ba)))
BY
{ (Auto THEN (InstLemma  `geo-axiom-contrapositive` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a⌝]⋅ THENA Auto) THEN D 0 THEN Auto) }

1
1. e : GeometryPrimitives
2. BasicGeometryAxioms(e)
3. a : Point
4. b : Point
5. a # a
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:GeometryPrimitives.  (BasicGeometryAxioms(e)  {}\mRightarrow{}  (\mforall{}a,b:Point.    (\mneg{}ab>ba)))


By

---

Latex:
(Auto  THEN  (InstLemma    `geo-axiom-contrapositive`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index