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 ;
hence the ToleranceRel of P is total by ORDERS_1:13; :: according to PCS_0:def 8 :: thesis: verum