let X be set ; :: thesis: bool X is Coherence_Space
A1: for A being set st A c= bool X & ( for a, b being set st a in A & b in A holds
a \/ b in bool X ) holds
union A in bool X

proof

let A be set ; :: thesis: ( A c= bool X & ( for a, b being set st a in A & b in A holds
a \/ b in bool X ) implies union A in bool X )
assume that
A2: A c= bool X and
for a, b being set st a in A & b in A holds
a \/ b in bool X ; :: thesis: union A in bool X
for a being set st a in A holds
a c= X by A2;
then union A c= X by ZFMISC_1:76;
hence union A in bool X ; :: thesis: verum

end;

for a, b being set st a in bool X & b c= a holds
b in bool X

proof

let a, b be set ; :: thesis: ( a in bool X & b c= a implies b in bool X )
assume ( a in bool X & b c= a ) ; :: thesis: b in bool X
then b c= X by XBOOLE_1:1;
hence b in bool X ; :: thesis: verum

end;

hence bool X is Coherence_Space by A1, Def1, CLASSES1:def 1; :: thesis: verum