let S be Subset of X; :: thesis: ( S is empty implies S is relatively-compact )
assume A1: S is empty ; :: thesis: S is relatively-compact
then Cl S = S by PRE_TOPC:22;
hence S is relatively-compact by A1, Def2; :: thesis: verum