let X, Y be set ; :: thesis: ( X is infinite & Y is finite implies X \ Y is infinite )

assume A1: ( X is infinite & Y is finite ) ; :: thesis: X \ Y is infinite

A2: X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39;

assume X \ Y is finite ; :: thesis: contradiction

hence contradiction by A1, A2, Th3; :: thesis: verum

assume A1: ( X is infinite & Y is finite ) ; :: thesis: X \ Y is infinite

A2: X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39;

assume X \ Y is finite ; :: thesis: contradiction

hence contradiction by A1, A2, Th3; :: thesis: verum