:: deftheorem Def3 defines TolSets TOLER_1:def 3 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ = TolSets T iff for Y being set holds
( Y in b₃ iff Y is TolSet of T ) );