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

( 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

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

( 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