theorem Th39: :: FINSEQ_3:41

for X being set
for k, l, m, n being Nat st X is included_in_Seg & k < l & 1 <= n & m <= len (Sgm X) & (Sgm X) . m = k & (Sgm X) . n = l holds
m < n