let n, m be natural number ; :: thesis: ( (idseq n) | (Seg m) = idseq n iff n <= m )
len (idseq n) = n by CARD_1:def 7;
hence ( (idseq n) | (Seg m) = idseq n iff n <= m ) by Th55; :: thesis: verum