let X, Y be set ; :: thesis: ( X is infinite implies X \/ Y is infinite )
assume A1: X is infinite ; :: thesis: X \/ Y is infinite
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