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 s .: () c= 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 s .: () c= 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 s .: () c= B )

let cB be basis of (); :: thesis: ( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st s .: () c= B )
hereby :: thesis: ( ( for B being Element of cB ex n being Nat st s .: () c= 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 s .: () c= B
hereby :: thesis: verum
let B be Element of cB; :: thesis: ex n being Nat st s .: () c= B
consider n being Nat such that
A2: square-uparrow n c= s " B by ;
take n = n; :: thesis: s .: () c= B
A3: s .: () c= s .: (s " B) by ;
s .: (s " B) c= B by FUNCT_1:75;
hence s .: () c= B by A3; :: thesis: verum
end;
end;
assume A4: for B being Element of cB ex n being Nat st s .: () c= B ; :: thesis:
now :: thesis: for B being Element of cB ex n being Nat st square-uparrow n c= s " B
let B be Element of cB; :: thesis: ex n being Nat st square-uparrow n c= s " B
consider n being Nat such that
A5: s .: () c= B by A4;
A6: s " (s .: ()) c= s " B by ;
dom s = by FUNCT_2:def 1;
then square-uparrow n c= s " (s .: ()) by FUNCT_1:76;
then square-uparrow n c= s " B by A6;
hence ex n being Nat st square-uparrow n c= s " B ; :: thesis: verum
end;
hence x in lim_filter (s,) by Th48; :: thesis: verum