let A, X, Y be set ; :: thesis: ( X c= A & Y c= A implies X \+\ Y c= A )
assume ( X c= A & Y c= A ) ; :: thesis: X \+\ Y c= A
then ( X \ Y c= A & Y \ X c= A ) by Th109;
hence X \+\ Y c= A by Th8; :: thesis: verum