let X be set ; :: thesis: ( X is c=directed implies for a, b being set st a in X & b in X holds
ex c being set st
( a \/ b c= c & c in X ) )
assume A1: for Y being finite Subset of X ex a being set st
( union Y c= a & a in X ) ; :: according to COHSP_1:def 4 :: thesis: for a, b being set st a in X & b in X holds
ex c being set st
( a \/ b c= c & c in X )
let a, b be set ; :: thesis: ( a in X & b in X implies ex c being set st
( a \/ b c= c & c in X ) )
assume ( a in X & b in X ) ; :: thesis: ex c being set st
( a \/ b c= c & c in X )
then A2: {a,b} is finite Subset of X by ZFMISC_1:32;
union {a,b} = a \/ b by ZFMISC_1:75;
hence ex c being set st
( a \/ b c= c & c in X ) by A1, A2; :: thesis: verum