let x, y be set ; :: thesis: {x,y,(x \/ y)} is c=directed
set X = {x,y,(x \/ y)};
let A be finite Subset of {x,y,(x \/ y)}; :: according to COHSP_1:def 4 :: thesis: ex a being set st
( union A c= a & a in {x,y,(x \/ y)} )
take a = x \/ y; :: thesis: ( union A c= a & a in {x,y,(x \/ y)} )
union {x,y,(x \/ y)} = a by Lm2;
hence union A c= a by ZFMISC_1:77; :: thesis: a in {x,y,(x \/ y)}
thus a in {x,y,(x \/ y)} by ENUMSET1:def 1; :: thesis: verum