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
( A in bool E & B in bool E ) by Def2;
then A1: ( A c= E & 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