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