for m, n being Nat holds
( n <= m iff Segm n c= Segm m )