for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone & x is_<=_than X holds
f . x is_<=_than f .: X