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

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 consider c being set such that
A1: ( a \/ b c= c & c in A ) by Th5;
thus a \/ b in C by A1, CLASSES1:def 1; :: thesis: verum

end;

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