for m, n being Nat holds
( (idseq n) | (Seg m) = idseq m iff m <= n )