theorem :: RELAT_1:184

for R, S being Relation holds
( R c= S iff R c= S | (dom R) )