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