let T be non empty TopSpace; :: thesis: for s being Function of , the carrier of T
for x being Point of T holds
( x in lim_filter (s,) iff for A being a_neighborhood of x holds \ (s " A) is finite )

let s be Function of , the carrier of T; :: thesis: for x being Point of T holds
( x in lim_filter (s,) iff for A being a_neighborhood of x holds \ (s " A) is finite )

let x be Point of T; :: thesis: ( x in lim_filter (s,) iff for A being a_neighborhood of x holds \ (s " A) is finite )
hereby :: thesis: ( ( for A being a_neighborhood of x holds \ (s " A) is finite ) implies x in lim_filter (s,) )
assume A1: x in lim_filter (s,) ; :: thesis: for A being a_neighborhood of x holds \ (s " A) is finite
now :: thesis: for A being a_neighborhood of x holds \ (s " A) is finite
let A be a_neighborhood of x; :: thesis: \ (s " A) is finite
ex B being finite Subset of st s " A = \ B by ;
hence [::] \ (s " A) is finite by Th1; :: thesis: verum
end;
hence for A being a_neighborhood of x holds \ (s " A) is finite ; :: thesis: verum
end;
assume A2: for A being a_neighborhood of x holds \ (s " A) is finite ; :: thesis: x in lim_filter (s,)
now :: thesis: for A being a_neighborhood of x ex B being finite Subset of st s " A = \ B
let A be a_neighborhood of x; :: thesis: ex B being finite Subset of st s " A = \ B
A3: dom s = by FUNCT_2:def 1;
[::] \ (s " A) is finite by A2;
hence ex B being finite Subset of st s " A = \ B by ; :: thesis: verum
end;
hence x in lim_filter (s,) by Th45; :: thesis: verum