let S be Subset-Family of X; :: thesis: ( S is compl-closed & S is cap-closed implies S is diff-closed )
assume that
A1: S is compl-closed and
A2: S is cap-closed ; :: thesis: S is diff-closed
let A, B be set ; :: according to FINSUB_1:def 3 :: thesis: ( not A in S or not B in S or A \ B in S )
assume that
A3: A in S and
A4: B in S ; :: thesis: A \ B in S
A5: A /\ (X \ B) = (A /\ X) \ B by XBOOLE_1:49
.= A \ B by A3, XBOOLE_1:28 ;
X \ B in S by A4, A1;
hence A \ B in S by A3, A5, A2; :: thesis: verum