Nuprl Definition : right-angles-congruent-axiom
right-angles-congruent-axiom(e) ==
∀a,b,c,x,y,z:Point. (((Rabc ∧ Rxyz) ∧ (x ≠ y ∧ y ≠ z) ∧ a ≠ b ∧ b ≠ c) ⇒ abc ≅a xyz)
Definitions occuring in Statement :
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
geo-sep: a ≠ b,
and: P ∧ Q,
implies: P ⇒ Q,
geo-point: Point,
all: ∀x:A. B[x]
FDL editor aliases :
right-angles-congruent-axiom
Latex:
right-angles-congruent-axiom(e) ==
\mforall{}a,b,c,x,y,z:Point. (((Rabc \mwedge{} Rxyz) \mwedge{} (x \mneq{} y \mwedge{} y \mneq{} z) \mwedge{} a \mneq{} b \mwedge{} b \mneq{} c) {}\mRightarrow{} abc \00D0\msuba{} xyz)
Date html generated:
2017_10_02-PM-03_27_18
Last ObjectModification:
2017_08_23-PM-03_37_30
Theory : euclidean!plane!geometry
Home
Index