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:39; :: thesis: verum