let f be Relation; :: thesis: ( f is pcs-Str-yielding implies ( f is TolStr-yielding & f is RelStr-yielding ) )
assume A1: f is pcs-Str-yielding ; :: thesis: ( f is TolStr-yielding & f is RelStr-yielding )
thus f is TolStr-yielding :: thesis: f is RelStr-yielding

proof

let y be set ; :: according to PCS_0:def 13 :: thesis: ( y in rng f implies y is TolStr )
thus ( y in rng f implies y is TolStr ) by A1, Def28; :: thesis: verum

end;

let y be set ; :: according to YELLOW_1:def 3 :: thesis: ( not y in proj2 f or y is RelStr )
thus ( not y in proj2 f or y is RelStr ) by A1, Def28; :: thesis: verum