:: deftheorem defines field RELAT_1:def 6 :
for R being Relation holds field R = (dom R) \/ (rng R);