let f be Relation; :: thesis: ( f is pcs-yielding implies f is pcs-Str-yielding )
assume A2: f is pcs-yielding ; :: thesis: f is pcs-Str-yielding
let y be set ; :: according to PCS_0:def 28 :: thesis: ( y in rng f implies y is pcs-Str )
thus ( y in rng f implies y is pcs-Str ) by A2, Def29; :: thesis: verum