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 ) )
set x = the Element of X;
defpred S₁[ 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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be 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;
set y = the Element of Y9;
A7: Y \ { the Element of Y9} c= union X by A4;
the Element of Y9 in Y ;
then consider Z9 being set such that
A8: the Element of Y9 in Z9 and
A9: Z9 in X by A4, TARSKI:def 4;
A10: (n + 1) - 1 = n by XCMPLX_1:26;
( { the Element of Y9} c= Y & card { the Element of Y9} = 1 ) by CARD_1:30, ZFMISC_1:31;
then card (Y \ { the Element of Y9}) = n by A5, A6, A10, CARD_2:44;
then consider Z being set such that
A11: Z in X and
A12: Y \ { the Element of Y9} 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in V )
A15: ( x in { the Element of Y9} or not x in { the Element of Y9} ) ;
assume x in Y ; :: thesis: x in V
then ( x = the Element of Y9 or x in Y \ { the Element of Y9} ) 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= the Element of X ;
hence ex Z being set st
( Z in X & Y c= Z ) ; :: thesis: verum

end;

A18: for n being Nat holds S₁[n] from NAT_1:sch 2(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