let z0 be Complex; :: thesis: for N being Neighbourhood of z0 holds z0 in N
let N be Neighbourhood of z0; :: thesis: z0 in N
consider g being Real such that
A1: 0 < g and
A2: { z where z is Complex : |.(z - z0).| < g } c= N by Def5;
|.(z0 - z0).| = 0 by COMPLEX1:44;
then z0 in { z where z is Complex : |.(z - z0).| < g } by A1;
hence z0 in N by A2; :: thesis: verum