let a be set ; :: thesis: for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
let C be Coherence_Space; :: thesis: ( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
defpred S₁[ object , object ] means {$1} = $2;
thus ( a in C implies for x, y being set st x in a & y in a holds
{x,y} in C ) :: thesis: ( ( for x, y being set st x in a & y in a holds
{x,y} in C ) implies a in C )

proof

assume A1: a in C ; :: thesis: for x, y being set st x in a & y in a holds
{x,y} in C
let x, y be set ; :: thesis: ( x in a & y in a implies {x,y} in C )
assume ( x in a & y in a ) ; :: thesis: {x,y} in C
then {x,y} c= a by ZFMISC_1:32;
hence {x,y} in C by A1, CLASSES1:def 1; :: thesis: verum

end;

A2: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z ;
consider X being set such that
A3: for x being object holds
( x in X iff ex y being object st
( y in a & S₁[y,x] ) ) from TARSKI:sch 1(A2);
assume A4: for x, y being set st x in a & y in a holds
{x,y} in C ; :: thesis: a in C
A5: for b, c being set st b in X & c in X holds
b \/ c in C

proof

let b, c be set ; :: thesis: ( b in X & c in X implies b \/ c in C )
assume that
A6: b in X and
A7: c in X ; :: thesis: b \/ c in C
consider z being object such that
A8: z in a and
A9: {z} = c by A3, A7;
consider y being object such that
A10: y in a and
A11: {y} = b by A3, A6;
{y,z} in C by A4, A10, A8;
hence b \/ c in C by A11, A9, ENUMSET1:1; :: thesis: verum

end;

A12: union X = a

proof

thus union X c= a :: according to XBOOLE_0:def 10 :: thesis: a c= union X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in a )
assume x in union X ; :: thesis: x in a
then consider Z being set such that
A13: x in Z and
A14: Z in X by TARSKI:def 4;
ex y being object st
( y in a & Z = {y} ) by A3, A14;
hence x in a by A13, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in union X )
assume x in a ; :: thesis: x in union X
then A15: {x} in X by A3;
x in {x} by TARSKI:def 1;
hence x in union X by A15, TARSKI:def 4; :: thesis: verum

end;

X c= C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in C )
assume x in X ; :: thesis: x in C
then consider y being object such that
A16: y in a and
A17: {y} = x by A3;
{y,y} in C by A4, A16;
hence x in C by A17, ENUMSET1:29; :: thesis: verum

end;

hence a in C by A5, A12, Def1; :: thesis: verum