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 by Def1;
then A1: A c= E by ZFMISC_1:def 1;
thus A /\ (B `) = (A /\ E) \ B by XBOOLE_1:49
.= A \ B by A1, XBOOLE_1:28 ; :: thesis: verum