set N = { y where y is Complex : |.(y - z0).| < 1 } ;
A1: { y where y is Complex : |.(y - z0).| < 1 } c= COMPLEX

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z0).| < 1 } or z in COMPLEX )
assume A2: z in { y where y is Complex : |.(y - z0).| < 1 } ; :: thesis: z in COMPLEX
consider y being Complex such that
A3: z = y and
|.(y - z0).| < 1 by A2;
thus z in COMPLEX by A3; :: thesis: verum

end;

take { y where y is Complex : |.(y - z0).| < 1 } ; :: thesis: ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) )
thus ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) ) by A1; :: thesis: verum