let R be Relation; :: thesis: ( R is empty implies R is homogeneous )
assume A1: R is empty ; :: thesis: R is homogeneous
thus dom R is with_common_domain by A1; :: according to MARGREL1:def 22 :: thesis: verum