set FV = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of : t is Tolerance of } ;

now

reconsider o = {} as Subset of by XBOOLE_1:2;
reconsider e = {} as Element of Toler_on_subsets X by Th30;
take m = [e,o]; :: thesis: m in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of : t is Tolerance of }
thus m in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of : t is Tolerance of } by TOLER_1:39; :: thesis: verum

end;

hence not TOL X is empty ; :: thesis: verum