:: deftheorem Def4 defines pseudocompact PSCOMP_1:def 4 :
for T being TopStruct holds
( T is pseudocompact iff for f being RealMap of T st f is continuous holds
f is bounded );