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 that
A1: ( card X c= card Y or card X in card Y ) and
A2: Y is finite ; :: thesis: X is finite
card X c= card Y by A1, ORDINAL1:def 2;
hence X is finite by A2; :: thesis: verum