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