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