let C be Coherence_Space; ( 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)
; Web C = Total (union C)
now 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 ;
( ( [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 )
( {x,y} in C implies [x,y] in t )assume
{x,y} in C
;
[x,y] in tthen
(
x in union C &
y in union C )
by A1, ZFMISC_1:32;
hence
[x,y] in t
by TOLER_1:2;
verum end;
hence
Web C = Total (union C)
by Th5; verum