let C, D be Coherence_Space; :: thesis: ( ( for a being set holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) & ( for a being set holds
( a in D iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) implies C = D )
assume that
A15: for a being set holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in E ) and
A16: for a being set holds
( a in D iff for x, y being set st x in a & y in a holds
[x,y] in E ) ; :: thesis: C = D
thus C c= D :: according to XBOOLE_0:def 10 :: thesis: D c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in D )
assume x in C ; :: thesis: x in D
then for z, y being set st z in x & y in x holds
[z,y] in E by A15;
hence x in D by A16; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in C )
assume x in D ; :: thesis: x in C
then for z, y being set st z in x & y in x holds
[z,y] in E by A16;
hence x in C by A15; :: thesis: verum