:: deftheorem Def2 defines natsubset-yielding LEXBFS:def 3 :
for f being Relation holds
( f is natsubset-yielding iff rng f c= bool NAT );