let Y be set ; :: thesis: ( Y is c=directed implies for X being finite Subset of (union Y) ex y being set st
( y in Y & X c= y ) )
set F = Y;
assume A1: Y is c=directed ; :: thesis: for X being finite Subset of (union Y) ex y being set st
( y in Y & X c= y )
let X be finite Subset of (union Y); :: thesis: ex y being set st
( y in Y & X c= y )
X /\ (union Y) = union (INTERSECTION ({X},Y)) by SETFAM_1:25;
then reconsider FF = INTERSECTION ({X},Y) as finite Subset-Family of X by Th60;
A2: X null (union Y) = union FF by SETFAM_1:25;
( Y \/ FF is c=directed & FF null Y c= Y \/ FF ) by Th63, Th64, A1;
then consider a being set such that
A3: ( union FF c= a & a in Y \/ FF ) by COHSP_1:def 4;
( a in Y or ( a in FF & FF is_finer_than Y ) ) by A3, Th64, XBOOLE_0:def 3;
then consider b being set such that
A4: ( b in Y & a c= b ) by SETFAM_1:def 2;
take b ; :: thesis: ( b in Y & X c= b )
thus ( b in Y & X c= b ) by A2, A3, A4; :: thesis: verum