:: deftheorem Def7 defines non-Empty WAYBEL_3:def 7 :
for f being Relation holds
( f is non-Empty iff for S being 1-sorted st S in rng f holds
not S is empty );