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 A being finite Subset of 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 A being finite Subset of 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 A being finite Subset of st s .: () c= B )

let cB be basis of (); :: thesis: ( x in lim_filter (s,) iff for B being Element of cB ex A being finite Subset of st s .: () c= B )
hereby :: thesis: ( ( for B being Element of cB ex A being finite Subset of 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 A being finite Subset of st s .: () c= B
hereby :: thesis: verum
let B be Element of cB; :: thesis: ex A being finite Subset of st s .: () c= B
consider A being finite Subset of such that
A2: s " B = \ A by ;
take A = A; :: thesis: s .: () c= B
thus s .: () c= B by ; :: thesis: verum
end;
end;
assume A3: for B being Element of cB ex A being finite Subset of st s .: () c= B ; :: thesis: x in lim_filter (s,)
for A being a_neighborhood of x holds \ (s " A) is finite
proof
let A be a_neighborhood of x; :: thesis: \ (s " A) is finite
A4: A is Element of BOOL2F by YELLOW19:2;
cB is filter_basis ;
then consider B being Element of cB such that
A5: B c= A by A4;
consider C being finite Subset of such that
A6: s .: () c= B by A3;
s .: () c= A by A6, A5;
then A7: s " (s .: ()) c= s " A by RELAT_1:143;
dom s = by FUNCT_2:def 1;
then [::] \ C c= s " (s .: ()) by FUNCT_1:76;
then [::] \ C c= s " A by A7;
then [::] \ (s " A) c= \ () by XBOOLE_1:34;
then [::] \ (s " A) c= /\ C by XBOOLE_1:48;
hence [::] \ (s " A) is finite ; :: thesis: verum
end;
hence x in lim_filter (s,) by Th46; :: thesis: verum