let X, Y be set ; :: thesis: ( X is countable & Y is countable implies X \+\ Y is countable )
assume ( X is countable & Y is countable ) ; :: thesis: X \+\ Y is countable
then ( X \ Y is countable & Y \ X is countable ) ;
hence X \+\ Y is countable by Th47; :: thesis: verum