:: deftheorem Def7 defines (--) PCS_0:def 7 :
for P being TolStr
for p, q being Element of P holds
( p (--) q iff [p,q] in the ToleranceRel of P );