let X, Y be set ; :: thesis: ( not X is finite implies not X \/ Y is finite )
assume A1: not X is finite ; :: thesis: not X \/ Y is finite
A2: card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
assume X \/ Y is finite ; :: thesis: contradiction
hence contradiction by A1, A2; :: thesis: verum