theorem :: COMPL_SP:20

for T being TopStruct st T is compact holds
T is countably_compact ;