let X be non empty set ; :: 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 ) ) implies X is c=directed )
assume A1: 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 ) ; :: thesis: X is c=directed
let Y be finite Subset of X; :: according to COHSP_1:def 4 :: thesis: ex a being set st
( union Y c= a & a in X )
defpred S₁[ set ] means ex a being set st
( union $1 c= a & a in X );
A2: Y is finite ;
consider a being Element of X;
union {} c= a by XBOOLE_1:2, ZFMISC_1:2;
then A3: S₁[ {} ] ;

A4: now

let x, B be set ; :: thesis: ( x in Y & B c= Y & S₁[B] implies S₁[B \/ {x}] )
assume A5: ( x in Y & B c= Y ) ; :: thesis: ( S₁[B] implies S₁[B \/ {x}] )
assume S₁[B] ; :: thesis: S₁[B \/ {x}]
then consider a being set such that
A6: ( union B c= a & a in X ) ;
consider c being set such that
A7: ( a \/ x c= c & c in X ) by A1, A5, A6;
thus S₁[B \/ {x}] :: thesis: verum

proof

take c ; :: thesis: ( union (B \/ {x}) c= c & c in X )
union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:96
.= (union B) \/ x by ZFMISC_1:31 ;
then union (B \/ {x}) c= a \/ x by A6, XBOOLE_1:9;
hence ( union (B \/ {x}) c= c & c in X ) by A7, XBOOLE_1:1; :: thesis: verum

end;

end;

thus S₁[Y] from FINSET_1:sch 2(A2, A3, A4); :: thesis: verum