let X be set ; :: thesis: {} in Toler_on_subsets X
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 {} in Toler_on_subsets X by A1, TARSKI:def 4; :: thesis: verum