let z0 be Complex; :: thesis: for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
A1: z0 in COMPLEX by XCMPLX_0:def 2;
let N1, N2 be Neighbourhood of z0; :: thesis: ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
consider a1 being Real such that
A2: 0 < a1 and
A3: { y where y is Complex : |.(y - z0).| < a1 } c= N1 by Def5;
consider a2 being Real such that
A4: 0 < a2 and
A5: { y where y is Complex : |.(y - z0).| < a2 } c= N2 by Def5;
set g = min (a1,a2);
take { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; :: thesis: ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 )
A6: min (a1,a2) <= a2 by XXREAL_0:17;
A7: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a2 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a2 } )
assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; :: thesis: z in { y where y is Complex : |.(y - z0).| < a2 }
then consider y being Complex such that
A8: z = y and
A9: |.(y - z0).| < min (a1,a2) ;
|.(y - z0).| < a2 by A6, A9, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a2 } by A8; :: thesis: verum

end;

A10: min (a1,a2) <= a1 by XXREAL_0:17;
A11: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a1 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a1 } )
assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; :: thesis: z in { y where y is Complex : |.(y - z0).| < a1 }
then consider y being Complex such that
A12: z = y and
A13: |.(y - z0).| < min (a1,a2) ;
|.(y - z0).| < a1 by A10, A13, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a1 } by A12; :: thesis: verum

end;

0 < min (a1,a2) by A2, A4, XXREAL_0:15;
hence ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 ) by A1, A3, A5, A11, A7, Th6, XBOOLE_1:1; :: thesis: verum