:: deftheorem Def3 defines with_tolerance ROUGHS_1:def 3 :
for P being RelStr holds
( P is with_tolerance iff the InternalRel of P is Tolerance of the carrier of P );