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

now :: thesis: ex m being object st m in { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y }

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

end;

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