let X, Y be set ; :: thesis: ( X is infinite implies X \/ Y is infinite )
card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
hence ( X is infinite implies X \/ Y is infinite ) ; :: thesis: verum