theorem :: FINSEQ_3:152

for X being set st X is included_in_Seg holds
for m, n being Element of NAT st m in dom (Sgm X) & n = (Sgm X) . m holds
m <= n