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