let R, Q be Relation; :: thesis: ( dom R = {} & dom Q = {} implies R = Q )
assume that
A1: dom R = {} and
A2: dom Q = {} ; :: thesis: R = Q
R = {} by A1;
hence R = Q by A2; :: thesis: verum