let C be Coherence_Space; for T being Tolerance of (union C) holds
( T = Web C iff for x, y being object holds
( [x,y] in T iff {x,y} in C ) )
let T be Tolerance of (union C); ( T = Web C iff for x, y being object holds
( [x,y] in T iff {x,y} in C ) )
thus
( T = Web C implies for x, y being object holds
( [x,y] in T iff {x,y} in C ) )
( ( for x, y being object holds
( [x,y] in T iff {x,y} in C ) ) implies T = Web C )proof
assume A1:
T = Web C
;
for x, y being object holds
( [x,y] in T iff {x,y} in C )
let x,
y be
object ;
( [x,y] in T iff {x,y} in C )
thus
(
[x,y] in T implies
{x,y} in C )
( {x,y} in C implies [x,y] in T )
A4:
(
x in {x,y} &
y in {x,y} )
by TARSKI:def 2;
assume
{x,y} in C
;
[x,y] in T
hence
[x,y] in T
by A1, A4, Def2;
verum
end;
assume A5:
for x, y being object holds
( [x,y] in T iff {x,y} in C )
; T = Web C
for x, y being object holds
( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
proof
let x,
y be
object ;
( [x,y] in T iff ex X being set st
( X in C & x in X & y in X ) )
thus
(
[x,y] in T implies ex
X being
set st
(
X in C &
x in X &
y in X ) )
( ex X being set st
( X in C & x in X & y in X ) implies [x,y] in T )proof
assume A6:
[x,y] in T
;
ex X being set st
( X in C & x in X & y in X )
take
{x,y}
;
( {x,y} in C & x in {x,y} & y in {x,y} )
thus
(
{x,y} in C &
x in {x,y} &
y in {x,y} )
by A5, A6, TARSKI:def 2;
verum
end;
given X being
set such that A7:
X in C
and A8:
(
x in X &
y in X )
;
[x,y] in T
{x,y} c= X
by A8, ZFMISC_1:32;
then
{x,y} in C
by A7, CLASSES1:def 1;
hence
[x,y] in T
by A5;
verum
end;
hence
T = Web C
by Def2; verum