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 :: thesis: for x, y being object holds
( ( [x,y] in Web (CohSp E) implies [x,y] in E ) & ( [x,y] in E implies [x,y] in Web (CohSp E) ) )

let x, y be object ; :: 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, Def3; :: 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:87;
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 that
A4: u in {x,y} and
A5: v in {x,y} ; :: thesis: [u,v] in E
A6: ( v = x or v = y ) by A5, TARSKI:def 2;
( u = x or u = y ) by A4, TARSKI:def 2;
hence [u,v] in E by A2, A3, A6, EQREL_1:6, TOLER_1:7; :: thesis: verum

end;

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

end;

hence Web (CohSp E) = E ; :: thesis: verum