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