let E be set ; :: thesis: for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
let A, B be Subset of E; :: thesis: (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
A in bool E by Def1;
then A1: A c= E by ZFMISC_1:def 1;
thus (A \+\ B) ` = (E \ (A \/ B)) \/ ((E /\ A) /\ B) by XBOOLE_1:102
.= (A /\ B) \/ (E \ (A \/ B)) by A1, XBOOLE_1:28
.= (A /\ B) \/ ((A `) /\ (B `)) by XBOOLE_1:53 ; :: thesis: verum