let S be Subset of T; :: thesis: ( S is Nbhd of x,T iff ex A being Subset of T st
( A is open & x in A & A c= S ) )

hereby :: thesis: ( ex A being Subset of T st
( A is open & x in A & A c= S ) implies S is Nbhd of x,T )

assume A1: S is a_neighborhood of x ; :: thesis: ex N being Element of bool the carrier of T st
( N is open & x in N & N c= S )
take N = Int S; :: thesis: ( N is open & x in N & N c= S )
thus N is open ; :: thesis: ( x in N & N c= S )
thus x in N by A1, CONNSP_2:def 1; :: thesis: N c= S
thus N c= S by TOPS_1:16; :: thesis: verum

end;

assume ex A being Subset of T st
( A is open & x in A & A c= S ) ; :: thesis: S is Nbhd of x,T
hence x in Int S by TOPS_1:22; :: according to CONNSP_2:def 1 :: thesis: verum