let CNS be ComplexNormSpace; :: thesis: for x0 being Point of CNS
for N being Neighbourhood of x0 holds x0 in N
let x0 be Point of CNS; :: 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 CNS : ||.(z - x0).|| < g } c= N by Def1;
||.(x0 - x0).|| = ||.(0. CNS).|| by RLVECT_1:15
.= 0 by CLVECT_1:102 ;
then x0 in { z where z is Point of CNS : ||.(z - x0).|| < g } by A1;
hence x0 in N by A2; :: thesis: verum