let T be non empty TopSpace; :: thesis: for x being Point of T
for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x in lim_filter F )
let x be Point of T; :: thesis: for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x in lim_filter F )
let F be Filter of the carrier of T; :: thesis: ( x is_a_convergence_point_of F,T iff x in lim_filter F )
consider F2 being proper Filter of (BoolePoset the carrier of T) such that
A1: F = F2 by Th37;
( F is_filter-finer_than NeighborhoodSystem x iff x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } )
proof
thus ( F is_filter-finer_than NeighborhoodSystem x implies x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ) ; :: thesis: ( x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } implies F is_filter-finer_than NeighborhoodSystem x )
assume x in { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ; :: thesis: F is_filter-finer_than NeighborhoodSystem x
then consider x0 being Point of T such that
A2: x = x0 and
A3: F is_filter-finer_than NeighborhoodSystem x0 ;
thus F is_filter-finer_than NeighborhoodSystem x by A2, A3; :: thesis: verum
end;
hence ( x is_a_convergence_point_of F,T iff x in lim_filter F ) by A1, YELLOW19:3; :: thesis: verum