cobool X is cup-closed

proof

let a, b be set ; :: according to FINSUB_1:def 1 :: thesis: ( not a in cobool X or not b in cobool X or a \/ b in cobool X )
assume ( a in cobool X & b in cobool X ) ; :: thesis: a \/ b in cobool X
then ( ( a = {} & b = {} ) or ( a = X & b = {} ) or ( a = {} & b = X ) or ( a = X & b = X ) ) by TARSKI:def 2;
hence a \/ b in cobool X by TARSKI:def 2; :: thesis: verum

end;

hence ex b₁ being cap-closed with_empty_element Subset-Family of X st b₁ is cup-closed ; :: thesis: verum