let a be set ; :: thesis: for C being Coherence_Space st ( for x, y being set st x in a & y in a holds
{x,y} in C ) holds
a c= union C
let C be Coherence_Space; :: thesis: ( ( for x, y being set st x in a & y in a holds
{x,y} in C ) implies a c= union C )
assume A1: for x, y being set st x in a & y in a holds
{x,y} in C ; :: thesis: a c= union C
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in union C )
assume x in a ; :: thesis: x in union C
then {x,x} in C by A1;
then A2: {x} in C by ENUMSET1:29;
x in {x} by TARSKI:def 1;
hence x in union C by A2, TARSKI:def 4; :: thesis: verum