let X, Y be finite set ; :: thesis: ( X c= Y implies card X <= card Y )
assume X c= Y ; :: thesis: card X <= card Y
then Segm (card X) c= Segm (card Y) by CARD_1:11;
hence card X <= card Y by Th27; :: thesis: verum