Nuprl Lemma : geo-gt-prim-irreflexive

∀e:GeometryPrimitives. (BasicGeometryAxioms(e) ⇒ (∀a,b:Point.  (¬ab>ba)))


Proof



Definitions occuring in Statement :  basic-geo-axioms: BasicGeometryAxioms(g),  geo-gt-prim: ab>cd,  geo-primitives: GeometryPrimitives,  geo-point: Point,  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  not: ¬A,  false: False,  member: t ∈ T,  uall: ∀[x:A]. B[x],  prop: ℙ
Latex:
\mforall{}e:GeometryPrimitives.  (BasicGeometryAxioms(e)  {}\mRightarrow{}  (\mforall{}a,b:Point.    (\mneg{}ab>ba)))


Date html generated: 2020_05_20-AM-09_41_46
Last ObjectModification: 2020_01_27-PM-05_24_26

Theory : euclidean!plane!geometry


Home Index