let T be non empty TopSpace; :: thesis: for s being sequence of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter )
let s be sequence of T; :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter )
let x be Point of T; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,(Frechet_Filter NAT)) iff B is_coarser_than s .: base_of_frechet_filter )
set F = filter_image (s,(Frechet_Filter NAT));

hereby :: thesis: ( B is_coarser_than s .: base_of_frechet_filter implies x in lim_filter (s,(Frechet_Filter NAT)) )

assume x in lim_filter (s,(Frechet_Filter NAT)) ; :: thesis: B is_coarser_than s .: base_of_frechet_filter
then consider x0 being Element of T such that
A1: x = x0 and
A2: filter_image (s,(Frechet_Filter NAT)) is_filter-finer_than NeighborhoodSystem x0 ;
BOOL2F (NeighborhoodSystem x) is_filter-coarser_than filter_image (s,(Frechet_Filter NAT)) by A1, A2;
hence B is_coarser_than s .: base_of_frechet_filter by Th19, Th27; :: thesis: verum

end;

assume A3: B is_coarser_than s .: base_of_frechet_filter ; :: thesis: x in lim_filter (s,(Frechet_Filter NAT))
BOOL2F (NeighborhoodSystem x) is_filter-coarser_than filter_image (s,(Frechet_Filter NAT)) by A3, Th19, Th27;
then filter_image (s,(Frechet_Filter NAT)) is_filter-finer_than NeighborhoodSystem x ;
hence x in lim_filter (s,(Frechet_Filter NAT)) ; :: thesis: verum