:: deftheorem Def1 defines TolSet TOLER_1:def 1 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ is TolSet of T iff for x, y being set st x in b₃ & y in b₃ holds
[x,y] in T );