theorem :: RELAT_1:186

for X being set
for R being Relation holds dom (X |` R) c= dom R by Th80, XTUPLE_0:8;