:: deftheorem DI defines included_in_Seg FINSEQ_1:def 13 :
for X being set holds
( X is included_in_Seg iff ex k being Nat st X c= Seg k );