:: deftheorem Def7 defines non-empty RELAT_1:def 9 :
for R being Relation holds
( R is non-empty iff not {} in rng R );