Nuprl Lemma : basic-geo-sep-sym
∀e:GeometryPrimitives. (BasicGeometryAxioms(e) 
⇒ (∀a,b:Point.  (a # b 
⇒ b # a)))
Proof
Definitions occuring in Statement : 
basic-geo-axioms: BasicGeometryAxioms(g)
, 
geo-sep: a # b
, 
geo-primitives: GeometryPrimitives
, 
geo-point: Point
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
geo-ge: ab ≥ cd
, 
not: ¬A
, 
false: False
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
geo-sep: a # b
, 
geo-congruent: ab ≅ cd
, 
basic-geo-axioms: BasicGeometryAxioms(g)
, 
and: P ∧ Q
, 
cand: A c∧ B
, 
geo-length-sep: ab # cd)
, 
or: P ∨ Q
, 
guard: {T}
Latex:
\mforall{}e:GeometryPrimitives.  (BasicGeometryAxioms(e)  {}\mRightarrow{}  (\mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)))
Date html generated:
2020_05_20-AM-09_41_56
Last ObjectModification:
2020_01_27-PM-10_41_43
Theory : euclidean!plane!geometry
Home
Index