theorem Th19: :: FINSEQ_3:19

for k, n being Nat holds Seg k, Seg n are_c=-comparable