theorem :: FUNCT_1:81

for X, Y being set
for R being Relation holds X /\ (R " Y) c= R " ((R .: X) /\ Y)