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