consider x being Real such that
A1: x in X by SUBSET_1:10;
thus not Inv X is empty by A1, Th28; :: thesis: verum