for L being with_infima Poset
for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone