set R = the non empty reflexive RelStr ;
set J = I --> the non empty reflexive RelStr ;
A1: rng (I --> the non empty reflexive RelStr ) c= { the non empty reflexive RelStr } by FUNCOP_1:13;
reconsider J = I --> the non empty reflexive RelStr as ManySortedSet of I ;
take J ; :: thesis: ( J is RelStr-yielding & J is non-Empty & J is reflexive-yielding )
thus J is RelStr-yielding ; :: thesis: ( J is non-Empty & J is reflexive-yielding )
thus J is non-Empty by A1, TARSKI:def 1; :: thesis: J is reflexive-yielding
let S be RelStr ; :: according to WAYBEL_3:def 8 :: thesis: ( S in rng J implies S is reflexive )
assume S in rng J ; :: thesis: S is reflexive
hence S is reflexive by A1, TARSKI:def 1; :: thesis: verum