let a, X be set ; :: thesis: ( a c= X implies Total a in Toler_on_subsets X )
set F = { (Toler Y) where Y is Subset of X : verum } ;
assume a c= X ; :: thesis: Total a in Toler_on_subsets X
then A1: Toler a in { (Toler Y) where Y is Subset of X : verum } ;
Total a in Toler a by Def15;
hence Total a in Toler_on_subsets X by A1, TARSKI:def 4; :: thesis: verum