let X be non empty set ; :: thesis: for Y being set st X is c=directed & Y c= union X & Y is finite holds
ex Z being set st
( Z in X & Y c= Z )
let Y be set ; :: thesis: ( X is c=directed & Y c= union X & Y is finite implies ex Z being set st
( Z in X & Y c= Z ) )
assume A1: X is c=directed ; :: thesis: ( not Y c= union X or not Y is finite or ex Z being set st
( Z in X & Y c= Z ) )
consider x being Element of X;
defpred S₁[ Element of NAT ] means for Y being set st Y c= union X & Y is finite & card Y = $1 holds
ex Z being set st
( Z in X & Y c= Z );
A2: S₁[ 0 ]

proof

let Y be set ; :: thesis: ( Y c= union X & Y is finite & card Y = 0 implies ex Z being set st
( Z in X & Y c= Z ) )
assume ( Y c= union X & Y is finite & card Y = 0 ) ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
then Y = {} ;
then Y c= x by XBOOLE_1:2;
hence ex Z being set st
( Z in X & Y c= Z ) ; :: thesis: verum

end;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let Y be set ; :: thesis: ( Y c= union X & Y is finite & card Y = n + 1 implies ex Z being set st
( Z in X & Y c= Z ) )
assume A5: ( Y c= union X & Y is finite & card Y = n + 1 ) ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
then reconsider Y' = Y as non empty set ;
consider y being Element of Y';
( {y} c= Y & card {y} = 1 & (n + 1) - 1 = n & Y \ {y} c= Y ) by CARD_1:50, XCMPLX_1:26, ZFMISC_1:37;
then ( card (Y \ {y}) = n & Y \ {y} c= union X & Y \ {y} is finite ) by A5, CARD_2:63, XBOOLE_1:1;
then consider Z being set such that
A6: ( Z in X & Y \ {y} c= Z ) by A4;
y in Y ;
then consider Z' being set such that
A7: ( y in Z' & Z' in X ) by A5, TARSKI:def 4;
consider V being set such that
A8: ( Z \/ Z' c= V & V in X ) by A1, A6, A7, Th5;
take V ; :: thesis: ( V in X & Y c= V )
thus V in X by A8; :: thesis: Y c= V
thus Y c= V :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in V )
assume A9: x in Y ; :: thesis: x in V
( x in {y} or not x in {y} ) ;
then ( x = y or x in Y \ {y} ) by A9, TARSKI:def 1, XBOOLE_0:def 5;
then x in Z \/ Z' by A6, A7, XBOOLE_0:def 3;
hence x in V by A8; :: thesis: verum

end;

end;

end;

A10: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
assume A11: ( Y c= union X & Y is finite ) ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
then reconsider Y' = Y as finite set ;
card Y = card Y' ;
hence ex Z being set st
( Z in X & Y c= Z ) by A10, A11; :: thesis: verum