theorem Th33: :: AFINSQ_2:33

for l, m, n, k being Nat
for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n