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

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