ex x being Real st x in X by SUBSET_1:10;
hence not - X is empty by Th14; :: thesis: verum