let f be Relation; :: thesis: ( f is pcs-yielding implies ( f is reflexive-yielding & f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding ) )
assume A3: f is pcs-yielding ; :: thesis: ( f is reflexive-yielding & f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding )
thus f is reflexive-yielding :: thesis: ( f is transitive-yielding & f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding )

proof

let y be RelStr ; :: according to WAYBEL_3:def 8 :: thesis: ( not y in proj2 f or y is reflexive )
thus ( not y in proj2 f or y is reflexive ) by A3, Def29; :: thesis: verum

end;

thus f is transitive-yielding :: thesis: ( f is pcs-tol-reflexive-yielding & f is pcs-tol-symmetric-yielding )

proof

let y be RelStr ; :: according to PCS_0:def 4 :: thesis: ( y in rng f implies y is transitive )
thus ( y in rng f implies y is transitive ) by A3, Def29; :: thesis: verum

end;

thus f is pcs-tol-reflexive-yielding :: thesis: f is pcs-tol-symmetric-yielding

proof

let y be TolStr ; :: according to PCS_0:def 16 :: thesis: ( y in rng f implies y is pcs-tol-reflexive )
thus ( y in rng f implies y is pcs-tol-reflexive ) by A3, Def29; :: thesis: verum

end;

let y be TolStr ; :: according to PCS_0:def 18 :: thesis: ( y in rng f implies y is pcs-tol-symmetric )
thus ( y in rng f implies y is pcs-tol-symmetric ) by A3, Def29; :: thesis: verum