let C be Coherence_Space; :: thesis: for T being Tolerance of (union C) holds
( T = Web C iff for x, y being set 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 set holds
( [x,y] in T iff {x,y} in C ) )
thus ( T = Web C implies for x, y being set holds
( [x,y] in T iff {x,y} in C ) ) :: thesis: ( ( for x, y being set 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 set holds
( [x,y] in T iff {x,y} in C )
let x, y be set ; :: 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 & x in X & y in X ) by A1, Def3;
{x,y} c= X by A2, ZFMISC_1:38;
hence {x,y} in C by A2, CLASSES1:def 1; :: thesis: verum

end;

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

end;

assume A4: for x, y being set holds
( [x,y] in T iff {x,y} in C ) ; :: thesis: T = Web C
for x, y being set 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 set ; :: 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 A5: [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 A4, A5, TARSKI:def 2; :: thesis: verum

end;

given X being set such that A6: ( X in C & x in X & y in X ) ; :: thesis: [x,y] in T
{x,y} c= X by A6, ZFMISC_1:38;
then {x,y} in C by A6, CLASSES1:def 1;
hence [x,y] in T by A4; :: thesis: verum

end;

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