:: deftheorem Def9 defines pcs-tol-reflexive PCS_0:def 9 :
for P being TolStr holds
( P is pcs-tol-reflexive iff the ToleranceRel of P is_reflexive_in the carrier of P );