let X be set ; :: thesis: for E being Tolerance of X holds Web (CohSp E) = E
let E be Tolerance of X; :: thesis: Web (CohSp E) = E

now

let x, y be set ; :: thesis: ( ( [x,y] in Web (CohSp E) implies [x,y] in E ) & ( [x,y] in E implies [x,y] in Web (CohSp E) ) )
thus ( [x,y] in Web (CohSp E) implies [x,y] in E ) :: thesis: ( [x,y] in E implies [x,y] in Web (CohSp E) )

proof

assume [x,y] in Web (CohSp E) ; :: thesis: [x,y] in E
then A1: {x,y} in CohSp E by Th5;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence [x,y] in E by A1, Def4; :: thesis: verum

end;

assume A2: [x,y] in E ; :: thesis: [x,y] in Web (CohSp E)
then A3: ( x in X & y in X ) by ZFMISC_1:106;
for u, v being set st u in {x,y} & v in {x,y} holds
[u,v] in E

proof

let u, v be set ; :: thesis: ( u in {x,y} & v in {x,y} implies [u,v] in E )
assume ( u in {x,y} & v in {x,y} ) ; :: thesis: [u,v] in E
then ( ( u = x or u = y ) & ( v = x or v = y ) ) by TARSKI:def 2;
hence [u,v] in E by A2, A3, EQREL_1:12, TOLER_1:27; :: thesis: verum

end;

then {x,y} in CohSp E by Def4;
hence [x,y] in Web (CohSp E) by Th5; :: thesis: verum

end;

hence Web (CohSp E) = E by RELAT_1:def 2; :: thesis: verum