let S be Subset-Family of X; :: thesis: ( S is cup-closed & S is compl-closed implies S is cap-closed )

assume A1: ( S is cup-closed & S is compl-closed ) ; :: thesis: S is cap-closed

let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in S or not B in S or A /\ B in S )

assume that

A2: A in S and

A3: B in S ; :: thesis: A /\ B in S

( X \ A in S & X \ B in S ) by A1, A2, A3;

then A4: (X \ A) \/ (X \ B) in S by A1;

A /\ B c= A by XBOOLE_1:17;

then A /\ B = X /\ (A /\ B) by A2, XBOOLE_1:1, XBOOLE_1:28

.= X \ (X \ (A /\ B)) by XBOOLE_1:48

.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;

hence A /\ B in S by A1, A4; :: thesis: verum

assume A1: ( S is cup-closed & S is compl-closed ) ; :: thesis: S is cap-closed

let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in S or not B in S or A /\ B in S )

assume that

A2: A in S and

A3: B in S ; :: thesis: A /\ B in S

( X \ A in S & X \ B in S ) by A1, A2, A3;

then A4: (X \ A) \/ (X \ B) in S by A1;

A /\ B c= A by XBOOLE_1:17;

then A /\ B = X /\ (A /\ B) by A2, XBOOLE_1:1, XBOOLE_1:28

.= X \ (X \ (A /\ B)) by XBOOLE_1:48

.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ;

hence A /\ B in S by A1, A4; :: thesis: verum