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

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

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

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

end;

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

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