let P be TolStr ; :: thesis: ( P is empty implies ( P is pcs-tol-reflexive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric ) )
assume A1: P is empty ; :: thesis: ( P is pcs-tol-reflexive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
thus the ToleranceRel of P is_reflexive_in the carrier of P by A1; :: according to PCS_0:def 9 :: thesis: ( P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
thus the ToleranceRel of P is_irreflexive_in the carrier of P by A1; :: according to PCS_0:def 10 :: thesis: P is pcs-tol-symmetric
thus the ToleranceRel of P is_symmetric_in the carrier of P by A1; :: according to PCS_0:def 11 :: thesis: verum