for X being NormedLinearTopSpace
for V being Subset of X holds
( V is compact iff for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V ) )