let R be Relation; :: thesis: ( R is empty implies R is {} -defined )
assume R is empty ; :: thesis: R is {} -defined
hence dom R c= {} ; :: according to RELAT_1:def 18 :: thesis: verum