theorem :: RELAT_1:130

for X being set
for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)