theorem :: ZFMISC_1:73
for A, B being set holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)