let C, D be Coherence_Space; :: thesis: ( Web C = Web D implies C = D )
assume A1: Web C = Web D ; :: 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 Web D by A1, Th7;
hence x in D by Th7; :: 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 Web C by A1, Th7;
hence x in C by Th7; :: thesis: verum