:: deftheorem Def1 defines is_valid_wrt NOMIN_7:def 1 :
for R1, R2 being Relation holds
( R1 is_valid_wrt R2 iff rng R1 c= dom R2 );