defpred S₁[ set ] means for x, y being set st x in $1 & y in $1 holds
[x,y] in E;
consider Z being set such that
A1: for x being set holds
( x in Z iff ( x in bool X & S₁[x] ) ) from XFAMILY:sch 1();
A2: for A being set st A c= Z & ( for a, b being set st a in A & b in A holds
a \/ b in Z ) holds
union A in Z

proof

let A be set ; :: thesis: ( A c= Z & ( for a, b being set st a in A & b in A holds
a \/ b in Z ) implies union A in Z )
assume that
A3: A c= Z and
A4: for a, b being set st a in A & b in A holds
a \/ b in Z ; :: thesis: union A in Z

A5: now :: thesis: for x, y being set st x in union A & y in union A holds
[x,y] in E

let x, y be set ; :: thesis: ( x in union A & y in union A implies [x,y] in E )
assume that
A6: x in union A and
A7: y in union A ; :: thesis: [x,y] in E
consider Y1 being set such that
A8: y in Y1 and
A9: Y1 in A by A7, TARSKI:def 4;
consider X1 being set such that
A10: x in X1 and
A11: X1 in A by A6, TARSKI:def 4;
A12: x in X1 \/ Y1 by A10, XBOOLE_0:def 3;
A13: y in X1 \/ Y1 by A8, XBOOLE_0:def 3;
X1 \/ Y1 in Z by A4, A11, A9;
hence [x,y] in E by A1, A12, A13; :: thesis: verum

end;

now :: thesis: for a being set st a in A holds
a c= X

let a be set ; :: thesis: ( a in A implies a c= X )
assume a in A ; :: thesis: a c= X
then a in bool X by A1, A3;
hence a c= X ; :: thesis: verum

end;

then union A c= X by ZFMISC_1:76;
hence union A in Z by A1, A5; :: thesis: verum

end;

A14: for a, b being set st a in Z & b c= a holds
b in Z

proof

let a, b be set ; :: thesis: ( a in Z & b c= a implies b in Z )
assume that
A15: a in Z and
A16: b c= a ; :: thesis: b in Z
a in bool X by A1, A15;
then A17: b c= X by A16, XBOOLE_1:1;
for x, y being set st x in b & y in b holds
[x,y] in E by A1, A15, A16;
hence b in Z by A1, A17; :: thesis: verum

end;

( S₁[ {} ] & {} c= X ) ;
then reconsider Z = Z as Coherence_Space by A1, A14, A2, Def1, CLASSES1:def 1;
take Z ; :: thesis: for a being set holds
( a in Z iff for x, y being set st x in a & y in a holds
[x,y] in E )
let a be set ; :: thesis: ( a in Z iff for x, y being set st x in a & y in a holds
[x,y] in E )
thus ( a in Z implies for x, y being set st x in a & y in a holds
[x,y] in E ) by A1; :: thesis: ( ( for x, y being set st x in a & y in a holds
[x,y] in E ) implies a in Z )
assume A18: for x, y being set st x in a & y in a holds
[x,y] in E ; :: thesis: a in Z
then a c= X by TOLER_1:18, TOLER_1:def 1;
hence a in Z by A1, A18; :: thesis: verum