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 ;
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