theorem :: RELAT_1:157

for X being set
for R being Relation holds R | X = R | ((dom R) /\ X)