:: deftheorem Def13 defines empty-yielding RELAT_1:def 15 :
for R being Relation holds
( R is empty-yielding iff rng R c= {{}} );