let f be homogeneous Relation; :: thesis: ( dom f = {{} } implies arity f = 0 )
assume dom f = {{} } ; :: thesis: arity f = 0
then {} in dom f by TARSKI:def 1;
hence arity f = 0 by CARD_1:47, MARGREL1:def 26; :: thesis: verum