set F = { (Toler Y) where Y is Subset of X : verum } ;
{} c= X ;
then A1: Toler {} in { (Toler Y) where Y is Subset of X : verum } ;
{} in Toler {} by Def15, TOLER_1:14;
hence not Toler_on_subsets X is empty by A1, TARSKI:def 4; :: thesis: verum