let a be set ; for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
let C be Coherence_Space; ( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
thus
( a in C implies for x, y being set st x in a & y in a holds
[x,y] in Web C )
( ( for x, y being set st x in a & y in a holds
[x,y] in Web C ) implies a in C )
assume A2:
for x, y being set st x in a & y in a holds
[x,y] in Web C
; a in C
hence
a in C
by Th6; verum