let T be non empty TopSpace; :: thesis:
let F be Filter of the carrier of T; :: thesis:

hereby :: thesis:

let x be object ; :: thesis:
assume x in lim_filter F ; :: thesis:
then consider x0 being Point of T such that
A1: x = x0 and
A2: F is_filter-finer_than NeighborhoodSystem x0 ;
thus x in lim_filterb (F2BOOL (F,T)) by A1, A2; :: thesis:

end;

let x be object ; :: thesis:
assume x in lim_filterb (F2BOOL (F,T)) ; :: thesis:
then consider x0 being Point of T such that
A3: x = x0 and
A4: NeighborhoodSystem x0 c= F ;
F is_filter-finer_than NeighborhoodSystem x0 by A4;
hence x in lim_filter F by A3; :: thesis:

end;

then ( lim_filter F c= lim_filterb (F2BOOL (F,T)) & lim_filterb (F2BOOL (F,T)) c= lim_filter F ) ;
hence lim_filter F = lim_filterb (F2BOOL (F,T)) ; :: thesis: