let X be RealNormSpace; :: thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; :: thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A1: for e being Real st e > 0 holds
||.x.|| < e ; :: thesis: x = 0. X
assume x <> 0. X ; :: thesis: contradiction
then 0 <> ||.x.|| by NORMSP_0:def 5;
hence contradiction by A1; :: thesis: verum