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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in CohSp (Web C) or x in C )
assume x in CohSp (Web C) ; :: thesis: x in C
then for y, z being set st y in x & z in x holds
[y,z] in Web C by Def4;
hence x in C by Th7; :: thesis: verum

end;

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