let C be Coherence_Space; :: thesis: for A being c=directed Subset of C holds union A in C
let A be c=directed Subset of C; :: thesis: union A in C

now :: thesis: for a, b being set st a in A & b in A holds
a \/ b in C

let a, b be set ; :: thesis: ( a in A & b in A implies a \/ b in C )
assume ( a in A & b in A ) ; :: thesis: a \/ b in C
then ex c being set st
( a \/ b c= c & c in A ) by Th5;
hence a \/ b in C by CLASSES1:def 1; :: thesis: verum

end;

hence union A in C by Def1; :: thesis: verum