let R be Relation; :: thesis: ( R is Poset-yielding implies ( R is RelStr-yielding & R is reflexive-yielding ) )
assume A1: for x being set st x in rng R holds
x is Poset ; :: according to YELLOW16:def 5 :: thesis: ( R is RelStr-yielding & R is reflexive-yielding )
hence for x being set st x in rng R holds
x is RelStr ; :: according to YELLOW_1:def 3 :: thesis: R is reflexive-yielding
thus for S being RelStr st S in rng R holds
S is reflexive by A1; :: according to WAYBEL_3:def 8 :: thesis: verum