let T be non empty TopSpace; :: thesis: for s being Function of , the carrier of T
for x being Point of T holds
( x in lim_filter (s,) iff for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B )

let s be Function of , the carrier of T; :: thesis: for x being Point of T holds
( x in lim_filter (s,) iff for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B )

let x be Point of T; :: thesis: ( x in lim_filter (s,) iff for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B )
set F = filter_image (s,);
A1: ( filter_image (s,) is_filter-finer_than NeighborhoodSystem x iff for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B )
proof
hereby :: thesis: ( ( for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B ) implies filter_image (s,) is_filter-finer_than NeighborhoodSystem x )
assume filter_image (s,) is_filter-finer_than NeighborhoodSystem x ; :: thesis: for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B
then NeighborhoodSystem x c= { M where M is Subset of the carrier of T : ex A being finite Subset of st s " M = \ A } by Th43;
then A2: { A where A is a_neighborhood of x : verum } c= { M where M is Subset of the carrier of T : ex A being finite Subset of st s " M = \ A } by YELLOW19:def 1;
thus for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B :: thesis: verum
proof
let A be a_neighborhood of x; :: thesis: ex B being finite Subset of st s " A = \ B
A in { A where A is a_neighborhood of x : verum } ;
then A in { M where M is Subset of the carrier of T : ex A being finite Subset of st s " M = \ A } by A2;
then ex M being Subset of the carrier of T st
( A = M & ex B being finite Subset of st s " M = \ B ) ;
hence ex B being finite Subset of st s " A = \ B ; :: thesis: verum
end;
end;
assume A3: for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B ; :: thesis:
NeighborhoodSystem x c= filter_image (s,)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NeighborhoodSystem x or y in filter_image (s,) )
assume y in NeighborhoodSystem x ; :: thesis:
then y in { A where A is a_neighborhood of x : verum } by YELLOW19:def 1;
then consider A being a_neighborhood of x such that
A4: y = A ;
ex B being finite Subset of st s " A = \ B by A3;
then A in { M where M is Subset of the carrier of T : ex A being finite Subset of st s " M = \ A } ;
hence y in filter_image (s,) by ; :: thesis: verum
end;
hence filter_image (s,) is_filter-finer_than NeighborhoodSystem x ; :: thesis: verum
end;
( filter_image (s,) is_filter-finer_than NeighborhoodSystem x iff x in lim_filter () )
proof end;
hence ( x in lim_filter (s,) iff for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B ) by A1; :: thesis: verum