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