theorem :: RELAT_1:69

for R being Relation holds R | (dom R) = R ;