:: deftheorem defines sequentially_compact TOPMETR4:def 2 :
for M being non empty MetrSpace holds
( M is sequentially_compact iff [#] M is sequentially_compact );