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