consider T being Tolerance of X;
T in Toler X by Def19;
hence not Toler X is empty ; :: thesis: verum