:: deftheorem Def5 defines Category-yielding_on_first INDEX_1:def 5 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Category-yielding_on_first iff IT `1 is Category-yielding );