let J be net_set of the carrier of Y,T; :: thesis: J is yielding_non-empty_carriers
let i be set ; :: according to YELLOW_6:def 2 :: thesis: ( i in rng J implies i is non empty 1-sorted )
assume i in rng J ; :: thesis: i is non empty 1-sorted
hence i is non empty 1-sorted by Def15; :: thesis: verum