let X be set ; :: thesis: [{},{}] in TOL X
( {} in Toler_on_subsets X & {} c= X ) by Th28;
hence [{},{}] in TOL X by TOLER_1:14; :: thesis: verum