Nuprl Lemma : geo-sep-sym
∀e:EuclideanPlane. ∀a,b:Point. (a ≠ b ⇒ b ≠ a)
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
euclidean-plane: EuclideanPlane,
implies: P ⇒ Q,
sq_stable: SqStable(P),
and: P ∧ Q,
squash: ↓T
Lemmas referenced :
basic-geo-sep-sym,
euclidean-plane_wf,
sq_stable__geo-axioms
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
setElimination,
rename,
hypothesisEquality,
hypothesis,
independent_functionElimination,
productElimination,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b:Point. (a \mneq{} b {}\mRightarrow{} b \mneq{} a)
Date html generated:
2017_10_02-PM-03_28_04
Last ObjectModification:
2017_09_29-AM-11_33_50
Theory : euclidean!plane!geometry
Home
Index