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 by A1; :: thesis: f is RelStr-yielding
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; :: thesis: verum