let X be set ; :: thesis: {} in Toler_on_subsets X
set F = { (Toler Y) where Y is Subset of X : verum } ;
{} c= X by XBOOLE_1:2;
then ( {} in Toler {} & Toler {} in { (Toler Y) where Y is Subset of X : verum } ) by Def19, TOLER_1:39;
hence {} in Toler_on_subsets X by TARSKI:def 4; :: thesis: verum