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