X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6;
hence X \+\ Y is ext-natural-membered ; :: thesis: verum