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