let a, X be set ; :: thesis: ( a c= X implies [(Total a),a] in TOL X )
assume A1: a c= X ; :: thesis: [(Total a),a] in TOL X
then Total a in Toler_on_subsets X by Th29;
hence [(Total a),a] in TOL X by A1; :: thesis: verum