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