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 A1: x in Lim (a_net (F2BOOL (F,T))) ; :: thesis:
then reconsider x0 = x as Point of T ;
F is_filter-finer_than NeighborhoodSystem x0 by A1, YELLOW19:3, YELLOW19:17;
hence x in lim_filter F ; :: thesis:

end;

let x be object ; :: thesis:
assume A2: x in lim_filter F ; :: thesis:
then reconsider x0 = x as Point of T ;
consider x1 being Point of T such that
A3: x0 = x1 and
A4: F is_filter-finer_than NeighborhoodSystem x1 by A2;
thus x in Lim (a_net (F2BOOL (F,T))) by A3, A4, YELLOW19:3, YELLOW19:17; :: thesis:

end;

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