let a be set ; :: thesis: 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; :: thesis: ( 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 ) :: thesis: ( ( for x, y being set st x in a & y in a holds
[x,y] in Web C ) implies a in C )

proof

assume A1: a in C ; :: thesis: for x, y being set st x in a & y in a holds
[x,y] in Web C
let x, y be set ; :: thesis: ( x in a & y in a implies [x,y] in Web C )
assume ( x in a & y in a ) ; :: thesis: [x,y] in Web C
then {x,y} in C by A1, Th6;
hence [x,y] in Web C by Th5; :: thesis: verum

end;

assume A2: for x, y being set st x in a & y in a holds
[x,y] in Web C ; :: thesis: a in C

now :: thesis: for x, y being set st x in a & y in a holds
{x,y} in C

let x, y be set ; :: thesis: ( x in a & y in a implies {x,y} in C )
assume ( x in a & y in a ) ; :: thesis: {x,y} in C
then [x,y] in Web C by A2;
hence {x,y} in C by Th5; :: thesis: verum

end;

hence a in C by Th6; :: thesis: verum