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