let p, q be FinSequence; :: thesis: ( p c= q implies len p <= len q )
assume p c= q ; :: thesis: len p <= len q
then Segm (card p) c= Segm (card q) by CARD_1:11;
hence len p <= len q by NAT_1:39; :: thesis: verum