:: deftheorem Def4 defines TolClasses TOLER_1:def 4 :
for X being set
for T being Tolerance of X
for b₃ being set holds
( b₃ = TolClasses T iff for Y being set holds
( Y in b₃ iff Y is TolClass of T ) );