:: deftheorem Def11 defines 1-sorted-yielding PRALG_1:def 11 :
for IT being Relation holds
( IT is 1-sorted-yielding iff for x being object st x in rng IT holds
x is 1-sorted );