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