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
assume A2: X \/ Y is finite ; :: thesis: contradiction
card X c= card (X \/ Y) by CARD_1:27, XBOOLE_1:7;
hence contradiction by A2, A1; :: thesis: verum