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
A19: 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
A20: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in D )
reconsider xx = x as set by TARSKI:1;
assume x in C ; :: thesis: x in D
then for z, y being set st z in xx & y in xx holds
[z,y] in E by A19;
hence x in D by A20; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in C )
reconsider xx = x as set by TARSKI:1;
assume x in D ; :: thesis: x in C
then for z, y being set st z in xx & y in xx holds
[z,y] in E by A20;
hence x in C by A19; :: thesis: verum