let S be reflexive RelStr ; :: thesis: 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))
let T be reflexive transitive RelStr ; :: thesis: for f being Function of S,T
for X being Subset of S holds downarrow (f .: X) c= downarrow (f .: (downarrow X))
let f be Function of S,T; :: thesis: for X being Subset of S holds downarrow (f .: X) c= downarrow (f .: (downarrow X))
let X be Subset of S; :: thesis: downarrow (f .: X) c= downarrow (f .: (downarrow X))
f .: X c= f .: (downarrow X) by RELAT_1:123, WAYBEL_0:16;
hence downarrow (f .: X) c= downarrow (f .: (downarrow X)) by YELLOW_3:6; :: thesis: verum