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