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 card X c= card Y by CARD_1:27;
hence card X <= card Y by Th40; :: thesis: verum