let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for cFXa, cFXb being Filter of X st cFXb is_filter-finer_than cFXa holds
filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa)
let f be Function of X,Y; :: thesis: for cFXa, cFXb being Filter of X st cFXb is_filter-finer_than cFXa holds
filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa)
let cFXa, cFXb be Filter of X; :: thesis: ( cFXb is_filter-finer_than cFXa implies filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa) )
assume A1: cFXb is_filter-finer_than cFXa ; :: thesis: filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa)
filter_image (f,cFXa) c= filter_image (f,cFXb)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in filter_image (f,cFXa) or x in filter_image (f,cFXb) )
assume x in filter_image (f,cFXa) ; :: thesis: x in filter_image (f,cFXb)
then ex M being Subset of Y st
( x = M & f " M in cFXa ) ;
hence x in filter_image (f,cFXb) by A1; :: thesis: verum

end;

hence filter_image (f,cFXb) is_filter-finer_than filter_image (f,cFXa) ; :: thesis: verum