let X be non empty TopSpace; :: thesis: for Y being non empty compact TopSpace
for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Y be non empty compact TopSpace; :: thesis: for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let x be Point of X; :: thesis: for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Z be Subset of [:Y,X:]; :: thesis: ( Z = [:([#] Y),{x}:] implies Z is compact )
reconsider V = {x} as non empty Subset of X ;
Y,[:Y,(X | V):] are_homeomorphic by Lm3;
then A1: [:Y,(X | V):] is compact by Th14;
assume A2: Z = [:([#] Y),{x}:] ; :: thesis: Z is compact
then TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #) by Lm4;
hence Z is compact by A2, A1, COMPTS_1:3; :: thesis: verum