let X be Subset of COMPLEX ; :: thesis: ( X is open implies for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X )
assume A1: X is open ; :: thesis: for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X
let z0 be Complex; :: thesis: ( z0 in X implies ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X )
assume z0 in X ; :: thesis: ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X
then consider N being Neighbourhood of z0 such that
A2: N c= X by A1, Th12;
consider g being Real such that
A3: ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= N ) by Def5;
take g ; :: thesis: { y where y is Complex : |.(y - z0).| < g } c= X
thus { y where y is Complex : |.(y - z0).| < g } c= X by A2, A3, XBOOLE_1:1; :: thesis: verum