set N = { y where y is Complex : |.(y - z0).| < 1 } ;
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 } ) )
{ y where y is Complex : |.(y - z0).| < 1 } c= COMPLEX

proof

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

end;

hence ( { 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 } ) ) ; :: thesis: verum