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

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