let X be RealNormSpace; :: thesis: for x, y being Point of X st ( for e being Real st e > 0 holds

||.(x - y).|| < e ) holds

x = y

let x, y be Point of X; :: thesis: ( ( for e being Real st e > 0 holds

||.(x - y).|| < e ) implies x = y )

assume for e being Real st e > 0 holds

||.(x - y).|| < e ; :: thesis: x = y

then x - y = 0. X by Lm1;

hence x = y by RLVECT_1:21; :: thesis: verum

||.(x - y).|| < e ) holds

x = y

let x, y be Point of X; :: thesis: ( ( for e being Real st e > 0 holds

||.(x - y).|| < e ) implies x = y )

assume for e being Real st e > 0 holds

||.(x - y).|| < e ; :: thesis: x = y

then x - y = 0. X by Lm1;

hence x = y by RLVECT_1:21; :: thesis: verum