let T be non empty TopSpace; :: thesis: for cF3, cF4 being Filter of the carrier of T st cF4 is_filter-finer_than cF3 holds
lim_filter cF3 c= lim_filter cF4
let cF3, cF4 be Filter of the carrier of T; :: thesis: ( cF4 is_filter-finer_than cF3 implies lim_filter cF3 c= lim_filter cF4 )
assume A1: cF4 is_filter-finer_than cF3 ; :: thesis: lim_filter cF3 c= lim_filter cF4
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_filter cF3 or x in lim_filter cF4 )
assume x in lim_filter cF3 ; :: thesis: x in lim_filter cF4
then consider y being Point of T such that
A2: x = y and
A3: cF3 is_filter-finer_than NeighborhoodSystem y ;
( NeighborhoodSystem y c= cF3 & cF3 c= cF4 ) by A1, A3;
then NeighborhoodSystem y c= cF4 ;
then cF4 is_filter-finer_than NeighborhoodSystem y ;
hence x in lim_filter cF4 by A2; :: thesis: verum