let m, n be Nat; :: 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 Th47; :: thesis: verum