the carrier of (One-Point_Compactification X) = succ ([#] X) by Def9;
hence not One-Point_Compactification X is empty ; :: thesis: verum