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

now

let x, y be set ; :: 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:106;
{x,y} c= union C

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in union C )
assume z in {x,y} ; :: thesis: z in union C
hence z in union C by A2, TARSKI:def 2; :: thesis: verum

end;

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:38;
hence [x,y] in t by TOLER_1:15; :: thesis: verum

end;

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