theorem :: FINSEQ_1:51

for X being set st ex k being Nat st X c= Seg k holds
( Sgm X = {} iff X = {} )