theorem :: WAYBEL_0:70

for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving