set R = the non empty 1-sorted ;
take I --> the non empty 1-sorted ; :: thesis: I --> the non empty 1-sorted is yielding_non-empty_carriers
let i be set ; :: according to YELLOW_6:def 2 :: thesis: ( i in rng (I --> the non empty 1-sorted ) implies i is non empty 1-sorted )
assume i in rng (I --> the non empty 1-sorted ) ; :: thesis: i is non empty 1-sorted
hence i is non empty 1-sorted by TARSKI:def 1; :: thesis: verum