set T = the Tolerance of X;
the Tolerance of X in Toler X by Def19;
hence not Toler X is empty ; :: thesis: verum