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, Th9;
consider g being Real such that
0 < g and
A3: { 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; :: thesis: verum