let T be non empty TopSpace; 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; 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; 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)); ( 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));
assume A3:
B is_coarser_than s .: base_of_frechet_filter
; 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))
; verum