let S be Subset-Family of X; :: thesis: ( S is compl-closed & S is cap-closed implies S is diff-closed )
assume that
Z1: S is compl-closed and
Z2: 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
A1: A in S and
A2: B in S ; :: thesis: A \ B in S
A3: A /\ (X \ B) = (A /\ X) \ B by XBOOLE_1:49
.= A \ B by A1, XBOOLE_1:28 ;
X \ B in S by A2, Z1, Def3;
hence A \ B in S by A1, A3, Z2, FINSUB_1:def 2; :: thesis: verum