ex x being Real st x in X by SUBSET_1:10;
hence not s ++ X is empty by Th20; :: thesis: verum