theorem :: RELAT_1:159

for X, Y being set holds rng [:X,Y:] c= Y