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

proof

let i be set ; :: according to PCS_0:def 16 :: thesis: ( i is TolStr & i in rng f implies i is pcs-tol-reflexive )
thus ( i is TolStr & i in rng f implies i is pcs-tol-reflexive ) by A1; :: thesis: verum

end;

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

proof

let i be set ; :: according to PCS_0:def 17 :: thesis: ( i is TolStr & i in rng f implies i is pcs-tol-irreflexive )
thus ( i is TolStr & i in rng f implies i is pcs-tol-irreflexive ) by A1; :: thesis: verum

end;

let i be set ; :: according to PCS_0:def 18 :: thesis: ( i is TolStr & i in rng f implies i is pcs-tol-symmetric )
thus ( i is TolStr & i in rng f implies i is pcs-tol-symmetric ) by A1; :: thesis: verum