for S being reflexive RelStr
for T being reflexive transitive RelStr
for f being Function of S,T
for X being Subset of S st f is monotone holds
downarrow (f .: X) = downarrow (f .: (downarrow X))