theorem :: FUNCT_1:70

for X, Y being set
for R being Relation holds (R | X) " Y = X /\ (R " Y)