:: deftheorem Def8 defines pcs-tol-total PCS_0:def 8 :
for P being TolStr holds
( P is pcs-tol-total iff the ToleranceRel of P is total );