let X, Y be set ; :: thesis: ( X is countable & Y is countable implies X \+\ Y is countable )
assume that
A1: X is countable and
A2: Y is countable ; :: thesis: X \+\ Y is countable
A3: X \ Y is countable by A1;
Y \ X is countable by A2;
hence X \+\ Y is countable by A3, Th84; :: thesis: verum