let z0 be Complex; :: thesis: for g being Real st 0 < g holds
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0
let g be Real; :: thesis: ( 0 < g implies { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 )
assume A1: g > 0 ; :: thesis: { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0
set N = { y where y is Complex : |.(y - z0).| < g } ;
A2: { y where y is Complex : |.(y - z0).| < g } c= COMPLEX

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z0).| < g } ; :: thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z0).| < g ) ;
hence z in COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

thus { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A1, A2, Def5; :: thesis: verum