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