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 )
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
A1: ( 0 < a1 & { y where y is Complex : |.(y - z0).| < a1 } c= N1 ) by Def5;
consider a2 being Real such that
A2: ( 0 < a2 & { y where y is Complex : |.(y - z0).| < a2 } c= N2 ) by Def5;
set g = min a1,a2;
A3: 0 < min a1,a2 by A1, A2, XXREAL_0:15;
A4: ( min a1,a2 <= a2 & min a1,a2 <= a1 ) by XXREAL_0:17;
A5: { 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 A6: z in { y where y is Complex : |.(y - z0).| < min a1,a2 } ; :: thesis: z in { y where y is Complex : |.(y - z0).| < a1 }
consider y being Complex such that
A7: ( z = y & |.(y - z0).| < min a1,a2 ) by A6;
|.(y - z0).| < a1 by A4, A7, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a1 } by A7; :: thesis: verum

end;

A8: { 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 A9: z in { y where y is Complex : |.(y - z0).| < min a1,a2 } ; :: thesis: z in { y where y is Complex : |.(y - z0).| < a2 }
consider y being Complex such that
A10: ( z = y & |.(y - z0).| < min a1,a2 ) by A9;
|.(y - z0).| < a2 by A4, A10, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a2 } by A10; :: thesis: verum

end;

take N = { y where y is Complex : |.(y - z0).| < min a1,a2 } ; :: thesis: ( N is Subset of COMPLEX & N is Neighbourhood of z0 & N c= N1 & N c= N2 )
thus ( N is Subset of COMPLEX & N is Neighbourhood of z0 & N c= N1 & N c= N2 ) by A1, A2, A3, A5, A8, Th8, XBOOLE_1:1; :: thesis: verum