Y,[:Y,(X | {x}):] are_homeomorphic by Lm3;
hence [:Y,(X | {x}):] is compact by Th16; :: thesis: verum