:: deftheorem defines \+\ XBOOLE_0:def 6 :
for X, Y being set holds X \+\ Y = (X \ Y) \/ (Y \ X);