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