let X be set ; for E being Tolerance of X holds Web (CohSp E) = E
let E be Tolerance of X; Web (CohSp E) = E
now 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 ;
( ( [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 )
( [x,y] in E implies [x,y] in Web (CohSp E) )assume A2:
[x,y] in E
;
[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 ;
( 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}
;
[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;
verum
end; then
{x,y} in CohSp E
by Def3;
hence
[x,y] in Web (CohSp E)
by Th5;
verum end;
hence
Web (CohSp E) = E
; verum