:: deftheorem defines compact NFCONT_1:def 2 :
for S being RealNormSpace
for X being Subset of S holds
( X is compact iff for s1 being sequence of S st rng s1 c= X holds
ex s2 being sequence of S st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );