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

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