theorem Th61: :: RELAT_1:67

for X being set
for R being Relation holds R | X = R /\ [:X,(rng R):]