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:27, MARGREL1:def 25; :: thesis: verum