let R, Q be Relation; :: thesis: ( dom R = {} & dom Q = {} implies R = Q )
assume ( dom R = {} & dom Q = {} ) ; :: thesis: R = Q
then ( R = {} & Q = {} ) ;
hence R = Q ; :: thesis: verum