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