theorem :: COMPTS_1:1

for T being TopStruct holds
( T is compact iff [#] T is compact ) ;