let R be Relation; :: thesis: ( R is Poset-yielding implies R is transitive-yielding )
assume A1: R is Poset-yielding ; :: thesis: R is transitive-yielding
let S be RelStr ; :: according to PCS_0:def 4 :: thesis: ( S in rng R implies S is transitive )
thus ( S in rng R implies S is transitive ) by A1, YELLOW16:def 5; :: thesis: verum