let T be non empty TopSpace; :: thesis: for x being Element of (InclPoset the topology of T) st x = the carrier of T holds
( x is compact iff T is compact )
let x be Element of (InclPoset the topology of T); :: thesis: ( x = the carrier of T implies ( x is compact iff T is compact ) )
assume A1: x = the carrier of T ; :: thesis: ( x is compact iff T is compact )
( T is compact iff [#] T is compact ) ;
hence ( x is compact iff T is compact ) by A1, Th36; :: thesis: verum