let S be Subset-Family of X; :: thesis: ( S is cap-closed & S is compl-closed implies S is cup-closed )
assume A5: ( S is cap-closed & S is compl-closed ) ; :: thesis: S is cup-closed
let A, B be set ; :: according to FINSUB_1:def 1 :: thesis: ( not A in S or not B in S or A \/ B in S )
assume A6: ( A in S & B in S ) ; :: thesis: A \/ B in S
then ( X \ A in S & X \ B in S ) by A5;
then A7: (X \ A) /\ (X \ B) in S by A5;
A \/ B = X /\ (A \/ B) by A6, XBOOLE_1:8, XBOOLE_1:28
.= X \ (X \ (A \/ B)) by XBOOLE_1:48
.= X \ ((X \ A) /\ (X \ B)) by XBOOLE_1:53 ;
hence A \/ B in S by A5, A7; :: thesis: verum