let T be non empty TopSpace; :: thesis: for F being Filter of the carrier of T holds lim_filter F = lim_filterb (F2BOOL (F,T))
let F be Filter of the carrier of T; :: thesis: lim_filter F = lim_filterb (F2BOOL (F,T))

now :: thesis: ( ( for x being object st x in lim_filter F holds
x in lim_filterb (F2BOOL (F,T)) ) & ( for x being object st x in lim_filterb (F2BOOL (F,T)) holds
x in lim_filter F ) )

hereby :: thesis: for x being object st x in lim_filterb (F2BOOL (F,T)) holds
x in lim_filter F

let x be object ; :: thesis: ( x in lim_filter F implies x in lim_filterb (F2BOOL (F,T)) )
assume x in lim_filter F ; :: thesis: x in lim_filterb (F2BOOL (F,T))
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: verum

end;

let x be object ; :: thesis: ( x in lim_filterb (F2BOOL (F,T)) implies x in lim_filter F )
assume x in lim_filterb (F2BOOL (F,T)) ; :: thesis: x in lim_filter F
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: verum

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: verum