let P be TolStr ; :: thesis: ( P is pcs-tol-reflexive implies P is pcs-tol-total )
assume P is pcs-tol-reflexive ; :: thesis: P is pcs-tol-total
then the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
then dom the ToleranceRel of P = the carrier of P by ORDERS_1:13;
hence the ToleranceRel of P is total by PARTFUN1:def 2; :: according to PCS_0:def 8 :: thesis: verum