theorem Th29: :: NAT_1:41

for m, n being Nat holds
( card (Segm n) in card (Segm m) iff n < m )