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