let T be non empty TopSpace; :: thesis: for s being Function of , the carrier of T
for x being Point of T
for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st square-uparrow n c= s " B )

let s be Function of , the carrier of T; :: thesis: for x being Point of T
for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st square-uparrow n c= s " B )

let x be Point of T; :: thesis: for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st square-uparrow n c= s " B )

let cB be basis of (); :: thesis: ( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st square-uparrow n c= s " B )
hereby :: thesis: ( ( for B being Element of cB ex n being Nat st square-uparrow n c= s " B ) implies x in lim_filter (s,) )
assume A1: x in lim_filter (s,) ; :: thesis: for B being Element of cB ex n being Nat st square-uparrow n c= s " B
hereby :: thesis: verum
let B be Element of cB; :: thesis: ex n being Nat st square-uparrow n c= s " B
B is a_neighborhood of x by YELLOW19:2;
hence ex n being Nat st square-uparrow n c= s " B by ; :: thesis: verum
end;
end;
assume A2: for B being Element of cB ex n being Nat st square-uparrow n c= s " B ; :: thesis:
now :: thesis: for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A
let A be a_neighborhood of x; :: thesis: ex n being Nat st square-uparrow n c= s " A
A3: A is Element of BOOL2F by YELLOW19:2;
cB is filter_basis ;
then consider B being Element of cB such that
A4: B c= A by A3;
A5: ex n being Nat st square-uparrow n c= s " B by A2;
s " B c= s " A by ;
hence ex n being Nat st square-uparrow n c= s " A by ; :: thesis: verum
end;
hence x in lim_filter (s,) by Th47; :: thesis: verum