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