let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
let x be Point of T; :: thesis: ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )
set F = filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).));
A1: ( filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A )

proof

hereby :: thesis: ( ( for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A ) implies filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x )

assume filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x ; :: thesis: for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A
then NeighborhoodSystem x c= { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } by Th44;
then A2: { A where A is a_neighborhood of x : verum } c= { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } by YELLOW19:def 1;
thus for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A :: thesis: verum

proof

let A be a_neighborhood of x; :: thesis: ex n being Nat st square-uparrow n c= s " A
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 n being Nat st square-uparrow n c= s " M } by A2;
then ex M being Subset of the carrier of T st
( A = M & ex n being Nat st square-uparrow n c= s " M ) ;
hence ex n being Nat st square-uparrow n c= s " A ; :: thesis: verum

end;

end;

assume A3: for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A ; :: thesis: filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x
NeighborhoodSystem x c= filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NeighborhoodSystem x or y in filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )
assume y in NeighborhoodSystem x ; :: thesis: y in filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
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 n being Nat st square-uparrow n c= s " A by A3;
then A in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } ;
hence y in filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by A4, Th44; :: thesis: verum

end;

hence filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x ; :: thesis: verum

end;

( filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x iff x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) )

proof

thus ( filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x implies x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) ) ; :: thesis: ( x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) implies filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x )
assume x in lim_filter (filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))) ; :: thesis: filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x
then ex y being Point of T st
( x = y & filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem y ) ;
hence filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) is_filter-finer_than NeighborhoodSystem x ; :: thesis: verum

end;

hence ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A ) by A1; :: thesis: verum