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 P is empty ; :: thesis: ( P is pcs-tol-reflexive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric )
then A1: TolStr(# the carrier of P,the ToleranceRel of P #) = emptyTolStr by Th2;
then A2: the carrier of P = field the ToleranceRel of P ;
hence the ToleranceRel of P is_reflexive_in the carrier of P by A1, RELAT_2:def 9; :: 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, A2, RELAT_2:def 10; :: 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, A2, RELAT_2:def 11; :: according to PCS_0:def 11 :: thesis: verum