:: deftheorem defines compact RCOMP_1:def 3 :
for X being Subset of REAL holds
( X is compact iff for s1 being Real_Sequence st rng s1 c= X holds
ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );