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 ) )
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 );
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 ) )

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: 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 that
A4: Y c= union X and
A5: Y is finite and
A6: card Y = n + 1 ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
reconsider Y9 = Y as non empty set by A6;
consider y being Element of Y9;
A7: Y \ {y} c= union X by A4, XBOOLE_1:1;
y in Y ;
then consider Z9 being set such that
A8: y in Z9 and
A9: Z9 in X by A4, TARSKI:def 4;
A10: (n + 1) - 1 = n by XCMPLX_1:26;
( {y} c= Y & card {y} = 1 ) by CARD_1:50, ZFMISC_1:37;
then card (Y \ {y}) = n by A5, A6, A10, CARD_2:63;
then consider Z being set such that
A11: Z in X and
A12: Y \ {y} c= Z by A3, A5, A7;
consider V being set such that
A13: Z \/ Z9 c= V and
A14: V in X by A1, A11, A9, Th5;
take V ; :: thesis: ( V in X & Y c= V )
thus V in X by A14; :: 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 )
A15: ( x in {y} or not x in {y} ) ;
assume x in Y ; :: thesis: x in V
then ( x = y or x in Y \ {y} ) by A15, TARSKI:def 1, XBOOLE_0:def 5;
then x in Z \/ Z9 by A12, A8, XBOOLE_0:def 3;
hence x in V by A13; :: thesis: verum

end;

end;

end;

A16: 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 that
Y c= union X and
Y is finite and
A17: card Y = 0 ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
Y = {} by A17;
then Y c= x by XBOOLE_1:2;
hence ex Z being set st
( Z in X & Y c= Z ) ; :: thesis: verum

end;

A18: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A16, A2);
assume that
A19: Y c= union X and
A20: Y is finite ; :: thesis: ex Z being set st
( Z in X & Y c= Z )
reconsider Y9 = Y as finite set by A20;
card Y = card Y9 ;
hence ex Z being set st
( Z in X & Y c= Z ) by A18, A19; :: thesis: verum