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