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 ;
assume A1: Z = [:([#] Y),{x}:] ; :: thesis: Z is compact
Y,[:Y,(X | V):] are_homeomorphic by Lm3;
then A2: [:Y,(X | V):] is compact by Th16;
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 A1, Lm4;
hence Z is compact by A1, A2, COMPTS_1:12; :: thesis: verum