:: deftheorem Def15 defines Toler COH_SP:def 16 :
for X, b₂ being set holds
( b₂ = Toler X iff for x being set holds
( x in b₂ iff x is Tolerance of X ) );