let C be Coherence_Space; :: thesis: 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); :: thesis: ( 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 ) ) :: thesis: ( ( 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 ; :: thesis: for x, y being object holds
( [x,y] in T iff {x,y} in C )
let x, y be object ; :: thesis: ( [x,y] in T iff {x,y} in C )
thus ( [x,y] in T implies {x,y} in C ) :: thesis: ( {x,y} in C implies [x,y] in T )

proof

assume [x,y] in T ; :: thesis: {x,y} in C
then consider X being set such that
A2: X in C and
A3: ( x in X & y in X ) by A1, Def2;
{x,y} c= X by A3, ZFMISC_1:32;
hence {x,y} in C by A2, CLASSES1:def 1; :: thesis: verum

end;

A4: ( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
assume {x,y} in C ; :: thesis: [x,y] in T
hence [x,y] in T by A1, A4, Def2; :: thesis: verum

end;

assume A5: for x, y being object holds
( [x,y] in T iff {x,y} in C ) ; :: thesis: 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 ; :: thesis: ( [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 ) ) :: thesis: ( 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 ; :: thesis: ex X being set st
( X in C & x in X & y in X )
take {x,y} ; :: thesis: ( {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; :: thesis: verum

end;

given X being set such that A7: X in C and
A8: ( x in X & y in X ) ; :: thesis: [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; :: thesis: verum

end;

hence T = Web C by Def2; :: thesis: verum