:: deftheorem Def10 defines pcs-tol-irreflexive PCS_0:def 10 :
for P being TolStr holds
( P is pcs-tol-irreflexive iff the ToleranceRel of P is_irreflexive_in the carrier of P );