let X, Y be set ; :: thesis: ( ( card X c= card Y or card X in card Y ) & Y is finite implies X is finite )
assume A1: ( ( card X c= card Y or card X in card Y ) & Y is finite ) ; :: thesis: X is finite
( card X c= card Y & card Y is finite ) by A1, ORDINAL1:def 2;
then ( card X is finite & X, card X are_equipotent ) by CARD_1:def 5;
hence X is finite ; :: thesis: verum