let T be non empty TopSpace; :: thesis: for A being Subset of T holds
( A is open iff for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A )
let A be Subset of T; :: thesis: ( A is open iff for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A )
thus ( A is open implies for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ) :: thesis: ( ( for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ) implies A is open )

proof

assume A1: A is open ; :: thesis: for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A
let x be Point of T; :: thesis: ( x in A implies ex B being Nbhd of x,T st B c= A )
assume x in A ; :: thesis: ex B being Nbhd of x,T st B c= A
then ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) by A1, CONNSP_2:7;
hence ex B being Nbhd of x,T st B c= A ; :: thesis: verum

end;

assume A2: for x being Point of T st x in A holds
ex B being Nbhd of x,T st B c= A ; :: thesis: A is open
for x being Point of T st x in A holds
ex B being Subset of T st
( B is a_neighborhood of x & B c= A )

proof

let x be Point of T; :: thesis: ( x in A implies ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) )
assume x in A ; :: thesis: ex B being Subset of T st
( B is a_neighborhood of x & B c= A )
then ex B being Nbhd of x,T st B c= A by A2;
hence ex B being Subset of T st
( B is a_neighborhood of x & B c= A ) ; :: thesis: verum

end;

hence A is open by CONNSP_2:7; :: thesis: verum