theorem :: RELAT_1:161

for Q, R being Relation st dom R = {} & dom Q = {} holds
R = Q ;