:: deftheorem Def2 defines yielding_non-empty_carriers YELLOW_6:def 2 :
for J being 1-sorted-yielding Function holds
( J is yielding_non-empty_carriers iff for i being set st i in rng J holds
i is non empty 1-sorted );