:: deftheorem Def16 defines -defined RELAT_1:def 18 :
for X being set
for R being Relation holds
( R is X -defined iff dom R c= X );