let T be non empty TopSpace; :: thesis: for x being Point of T
for F being upper Subset of (BoolePoset ([#] T)) holds
( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )
let x be Point of T; :: thesis: for F being upper Subset of (BoolePoset ([#] T)) holds
( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )
let F be upper Subset of (BoolePoset ([#] T)); :: thesis: ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )

hereby :: thesis: ( NeighborhoodSystem x c= F implies x is_a_convergence_point_of F,T )

assume A1: x is_a_convergence_point_of F,T ; :: thesis: NeighborhoodSystem x c= F
thus NeighborhoodSystem x c= F :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in NeighborhoodSystem x or y in F )
assume y in NeighborhoodSystem x ; :: thesis: y in F
then reconsider y = y as a_neighborhood of x by Th3;
x in Int y by CONNSP_2:def 1;
then A2: Int y in F by A1, WAYBEL_7:def 5;
Int y c= y by TOPS_1:16;
hence y in F by A2, WAYBEL_7:7; :: thesis: verum

end;

end;

assume A3: NeighborhoodSystem x c= F ; :: thesis: x is_a_convergence_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in F )
assume that
A4: A is open and
A5: x in A ; :: thesis: A in F
A is a_neighborhood of x by A4, A5, CONNSP_2:3;
then A in NeighborhoodSystem x ;
hence A in F by A3; :: thesis: verum