theorem Th39: :: FINSEQ_3:41

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