let C be Coherence_Space; :: thesis: ( C = bool (union C) implies Web C = Total (union C) )
reconsider t = Total (union C) as Tolerance of (union C) ;
assume A1: C = bool (union C) ; :: thesis: Web C = Total (union C)

now :: thesis: for x, y being object holds
( ( [x,y] in t implies {x,y} in C ) & ( {x,y} in C implies [x,y] in t ) )

let x, y be object ; :: thesis: ( ( [x,y] in t implies {x,y} in C ) & ( {x,y} in C implies [x,y] in t ) )
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 A2: ( x in union C & y in union C ) by ZFMISC_1:87;
{x,y} c= union C by A2, TARSKI:def 2;
hence {x,y} in C by A1; :: thesis: verum

end;

assume {x,y} in C ; :: thesis: [x,y] in t
then ( x in union C & y in union C ) by A1, ZFMISC_1:32;
hence [x,y] in t by TOLER_1:2; :: thesis: verum

end;

hence Web C = Total (union C) by Th5; :: thesis: verum