theorem :: RELAT_1:60
for X being set
for R being Relation holds dom (R | X) c= dom R by Th51;