let C be Coherence_Space; :: thesis: CohSp (Web C) = C
thus CohSp (Web C) c= C :: according to XBOOLE_0:def 10 :: thesis: C c= CohSp (Web C)

proof

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

end;

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