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
set a = the Element of X;
defpred S1[ set ] means ex a being set st
( union $1 c= a & a in X );
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 )
A2: now :: thesis: for x, B being set st x in Y & B c= Y & S1[B] holds
S1[B \/ {x}]
let x, B be set ; :: thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in Y and
B c= Y ; :: thesis: ( S1[B] implies S1[B \/ {x}] )
assume S1[B] ; :: thesis: S1[B \/ {x}]
then consider a being set such that
A4: union B c= a and
A5: a in X ;
consider c being set such that
A6: ( a \/ x c= c & c in X ) by A1, A3, A5;
thus S1[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:78
.= (union B) \/ x by ZFMISC_1:25 ;
then union (B \/ {x}) c= a \/ x by A4, XBOOLE_1:9;
hence ( union (B \/ {x}) c= c & c in X ) by A6; :: thesis: verum
end;
end;
union {} c= the Element of X by ZFMISC_1:2;
then A7: S1[ {} ] ;
A8: Y is finite ;
thus S1[Y] from FINSET_1:sch 2(A8, A7, A2); :: thesis: verum