x \ Y c= X \ y by XBOOLE_1:35;
hence for b₁ being set st b₁ = (x \ Y) \ (X \ y) holds
b₁ is empty ; :: thesis: verum