let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A )
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A )
let x be Point of T; :: thesis: for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A )
let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A )

hereby :: thesis: ( ( for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A1: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) ; :: thesis: for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A

hereby :: thesis: verum

let B be Element of cB; :: thesis: ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A
B is a_neighborhood of x by YELLOW19:2;
hence ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A by A1, Th45; :: thesis: verum

end;

end;

assume A2: for B being Element of cB ex A being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ A ; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))

now :: thesis: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite

let A be a_neighborhood of x; :: thesis: [:NAT,NAT:] \ (s " A) is finite
A3: A is Element of BOOL2F (NeighborhoodSystem x) by YELLOW19:2;
cB is filter_basis ;
then consider B being Element of cB such that
A4: B c= A by A3;
ex C being finite Subset of [:NAT,NAT:] st s " B = [:NAT,NAT:] \ C by A2;
hence [:NAT,NAT:] \ (s " A) is finite by A4, RELAT_1:145, Th1; :: thesis: verum

end;

hence x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) by Th46; :: thesis: verum