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