theorem :: RELAT_1:128

for X, Y being set
for R being Relation holds (R | X) .: Y c= R .: Y by Th53, Th116;