let F be net_set of X,T; :: thesis: F is yielding_non-empty_carriers
let v be set ; :: according to YELLOW_6:def 4 :: thesis: ( v in rng F implies v is non empty 1-sorted )
assume v in rng F ; :: thesis: v is non empty 1-sorted
hence v is non empty 1-sorted by Def15; :: thesis: verum