let X be non empty TopSpace; :: thesis: for Y being non empty compact TopSpace
for x being Point of X holds [:Y,(X | {x}):] is compact
let Y be non empty compact TopSpace; :: thesis: for x being Point of X holds [:Y,(X | {x}):] is compact
let x be Point of X; :: thesis: [:Y,(X | {x}):] is compact
Y,[:Y,(X | {x}):] are_homeomorphic by Lm3;
hence [:Y,(X | {x}):] is compact by Th16; :: thesis: verum