set D = cobool X;
for x, y being set st x in cobool X & y in cobool X holds
x /\ y in cobool X

proof

let x, y be set ; :: thesis: ( x in cobool X & y in cobool X implies x /\ y in cobool X )
assume ( x in cobool X & y in cobool X ) ; :: thesis: x /\ y in cobool X

per cases then ( x = {} or ( x = X & y = X ) or ( x = X & y = {} ) ) by TARSKI:def 2;

suppose x = {} ; :: thesis: x /\ y in cobool X

hence x /\ y in cobool X by TARSKI:def 2; :: thesis: verum

end;

suppose ( x = X & y = X ) ; :: thesis: x /\ y in cobool X

hence x /\ y in cobool X by TARSKI:def 2; :: thesis: verum

end;

suppose ( x = X & y = {} ) ; :: thesis: x /\ y in cobool X

hence x /\ y in cobool X by TARSKI:def 2; :: thesis: verum

end;

end;

end;

hence cobool X is cap-closed ; :: thesis: verum