:: deftheorem Def1 defines finitary PROOFS_1:def 1 :
for R being Relation holds
( R is finitary iff for a being object st a in dom R holds
a is finite set );