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, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) 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, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) 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, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B )

let cB be basis of (); :: thesis: ( x in lim_filter (s,) iff for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B )
hereby :: thesis: ( ( for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B ) implies x in lim_filter (s,) )
assume A1: x in lim_filter (s,) ; :: thesis: for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B
now :: thesis: for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B
let B be Element of cB; :: thesis: ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B
consider A being finite Subset of such that
A2: s .: () c= B by ;
consider n, m being Nat such that
A3: A c= [:(Segm n),(Segm m):] by Th16;
[::] \ [:(Segm n),(Segm m):] c= \ A by ;
then s .: ( \ [:(Segm n),(Segm m):]) c= s .: () by RELAT_1:123;
then s .: ( \ [:(Segm n),(Segm m):]) c= B by A2;
hence ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B ; :: thesis: verum
end;
hence for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B ; :: thesis: verum
end;
assume A4: for B being Element of cB ex n, m being Nat st s .: ( \ [:(Segm n),(Segm m):]) c= B ; :: thesis: x in lim_filter (s,)
now :: thesis: for B being Element of cB ex A being finite Subset of st s .: () c= B
let B be Element of cB; :: thesis: ex A being finite Subset of st s .: () c= B
consider n, m being Nat such that
A5: s .: ( \ [:(Segm n),(Segm m):]) c= B by A4;
reconsider A = [:(Segm n),(Segm m):] as finite Subset of ;
thus ex A being finite Subset of st s .: () c= B by A5; :: thesis: verum
end;
hence x in lim_filter (s,) by Th51; :: thesis: verum