for x, X being set holds
( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )