let a, X be set ; :: thesis: ( a c= X implies [(id a),a] in TOL X )
assume a c= X ; :: thesis: [(id a),a] in TOL X
then ( id a in Toler_on_subsets X & a in bool X & id a is Tolerance of a ) by Th32;
hence [(id a),a] in TOL X ; :: thesis: verum