let S be RealNormSpace; :: thesis: for x0 being Point of S
for N being Neighbourhood of x0 holds x0 in N
let x0 be Point of S; :: thesis: for N being Neighbourhood of x0 holds x0 in N
let N be Neighbourhood of x0; :: thesis: x0 in N
consider g being Real such that
A1: 0 < g and
A2: { z where z is Point of S : ||.(z - x0).|| < g } c= N by Def1;
||.(x0 - x0).|| = ||.(0. S).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
then x0 in { z where z is Point of S : ||.(z - x0).|| < g } by A1;
hence x0 in N by A2; :: thesis: verum