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