for S1, S2 being RelStr
for D being Subset of S1
for f being Function of S1,S2 st f is monotone holds
f .: (uparrow D) c= uparrow (f .: D)