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