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

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

per cases by TARSKI:def 2;

suppose x = {} ; :: thesis:

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

end;

suppose ( x = X & y = X ) ; :: thesis:

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

end;

suppose ( x = X & y = {} ) ; :: thesis:

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

end;

end;

end;

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