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