let A be set ; :: thesis:
assume A1: A is finite ; :: thesis:
let X be Subset-Family of A; :: thesis:
assume A2: X <> {} ; :: thesis:
consider p being Function such that
A3: rng p = A and
A4: dom p in omega by A1, Def1;
defpred S₁[ set ] means p .: $1 in X;
consider G being set such that
A5: for x being set holds
( x in G iff ( x in bool (dom p) & S₁[x] ) ) from XBOOLE_0:sch 1();
G c= bool (dom p)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in G ; :: thesis:
hence x in bool (dom p) by A5; :: thesis:

end;

then reconsider GX = G as Subset-Family of (dom p) ;
set x = the Element of X;
the Element of X is Subset of A by A2, TARSKI:def 3;
then A6: p .: (p " the Element of X) = the Element of X by A3, FUNCT_1:77;
p " the Element of X c= dom p by RELAT_1:132;
then A7: GX <> {} by A2, A5, A6;
defpred S₂[ set ] means ( $1 in omega implies for X being Subset-Family of $1 st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) );
A8: S₂[ {} ]

proof

assume {} in omega ; :: thesis:
let X be Subset-Family of {}; :: thesis:
assume X <> {} ; :: thesis:
then A9: X = {{}} by ZFMISC_1:1, ZFMISC_1:33;
take {} ; :: thesis:
thus ( {} in X & ( for B being set st B in X & {} c= B holds
B = {} ) ) by A9, TARSKI:def 1; :: thesis:

end;

A10: for O being Ordinal st S₂[O] holds
S₂[ succ O]

proof

let O be Ordinal; :: thesis:
assume A11: ( O in omega implies for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) ; :: thesis:
thus ( succ O in omega implies for X being Subset-Family of (succ O) st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ) :: thesis:

proof

assume succ O in omega ; :: thesis:
then A12: succ O c= omega by ORDINAL1:def 2;
let X be Subset-Family of (succ O); :: thesis:
assume A13: X <> {} ; :: thesis:
defpred S₃[ set ] means ex A being set st
( A in X & $1 = A \ {O} );
consider X1 being set such that
A14: for x being set holds
( x in X1 iff ( x in bool O & S₃[x] ) ) from XBOOLE_0:sch 1();
X1 c= bool O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in X1 ; :: thesis:
hence x in bool O by A14; :: thesis:

end;

then reconsider X2 = X1 as Subset-Family of O ;
set y = the Element of X;
A15: succ O = O \/ {O} by ORDINAL1:def 1;
the Element of X is Subset of (succ O) by A13, TARSKI:def 3;
then the Element of X \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then A16: the Element of X \ {O} c= O \ {O} by XBOOLE_1:40;
A17: O in succ O by ORDINAL1:6;
A18: not O in O ;
then the Element of X \ {O} c= O by A16, ZFMISC_1:57;
then X2 <> {} by A13, A14;
then consider Z being set such that
A19: Z in X2 and
A20: for B being set st B in X2 & Z c= B holds
B = Z by A11, A12, A17;
consider X1 being set such that
A21: X1 in X and
A22: Z = X1 \ {O} by A14, A19;
A23: O in {O} by TARSKI:def 1;
then A24: not O in Z by A22, XBOOLE_0:def 5;

A25: now

assume A26: Z \/ {O} in X ; :: thesis:
take A = Z \/ {O}; :: thesis:
for B being set st B in X & A c= B holds
B = A

proof

let B be set ; :: thesis:
assume A27: B in X ; :: thesis:
assume A28: A c= B ; :: thesis:

A29: now

assume A30: O in B ; :: thesis:
set Y = B \ {O};
{O} c= B by A30, ZFMISC_1:31;
then A31: B = (B \ {O}) \/ {O} by XBOOLE_1:45;
A \ {O} c= B \ {O} by A28, XBOOLE_1:33;
then A32: Z \ {O} c= B \ {O} by XBOOLE_1:40;
not O in Z by A22, A23, XBOOLE_0:def 5;
then A33: Z c= B \ {O} by A32, ZFMISC_1:57;
B \ {O} c= (O \/ {O}) \ {O} by A15, A27, XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A18, ZFMISC_1:57;
then B \ {O} in X2 by A14, A27;
hence B = A by A20, A31, A33; :: thesis:

end;

now

assume A34: not O in B ; :: thesis:
O in {O} by TARSKI:def 1;
then O in A by XBOOLE_0:def 3;
hence contradiction by A28, A34; :: thesis:

end;

hence B = A by A29; :: thesis:

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A26; :: thesis:

end;

now

assume A35: not Z \/ {O} in X ; :: thesis:
take A = Z; :: thesis:

now

assume O in X1 ; :: thesis:
then X1 = X1 \/ {O} by ZFMISC_1:40
.= Z \/ {O} by A22, XBOOLE_1:39 ;
hence contradiction by A21, A35; :: thesis:

end;

then A36: A in X by A21, A22, ZFMISC_1:57;
for B being set st B in X & A c= B holds
B = A

proof

let B be set ; :: thesis:
assume A37: B in X ; :: thesis:
then B \ {O} c= (O \/ {O}) \ {O} by A15, XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A18, ZFMISC_1:57;
then A38: B \ {O} in X2 by A14, A37;
assume A39: A c= B ; :: thesis:
then A \ {O} c= B \ {O} by XBOOLE_1:33;
then A40: A c= B \ {O} by A24, ZFMISC_1:57;

A41: now

assume A42: O in B ; :: thesis:
A \/ {O} = (B \ {O}) \/ {O} by A20, A38, A40
.= B \/ {O} by XBOOLE_1:39
.= B by A42, ZFMISC_1:40 ;
hence contradiction by A35, A37; :: thesis:

end;

A43: B c= O

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A44: x in B ; :: thesis:
( x in O or x in {O} ) by A15, A37, A44, XBOOLE_0:def 3;
hence x in O by A41, A44, TARSKI:def 1; :: thesis:

end;

B \ {O} = B by A41, ZFMISC_1:57;
then B in X2 by A14, A37, A43;
hence B = A by A20, A39; :: thesis:

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A36; :: thesis:

end;

hence ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) by A25; :: thesis:

end;

A45: for O being Ordinal st O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S₂[B] ) holds
S₂[O]

proof

let O be Ordinal; :: thesis:
assume that
A46: O <> {} and
A47: O is limit_ordinal and
for B being Ordinal st B in O holds
S₂[B] and
A48: O in omega ; :: thesis:
{} in O by A46, ORDINAL1:14;
then omega c= O by A47, ORDINAL1:def 11;
then O in O by A48;
hence for X being Subset-Family of O st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) ) ; :: thesis:

end;

for O being Ordinal holds S₂[O] from ORDINAL2:sch 1(A8, A10, A45);
then consider g being set such that
A49: g in GX and
A50: for B being set st B in GX & g c= B holds
B = g by A4, A7;
take p .: g ; :: thesis:
for B being set st B in X & p .: g c= B holds
B = p .: g

proof

let B be set ; :: thesis:
assume A51: B in X ; :: thesis:
assume p .: g c= B ; :: thesis:
then A52: p " (p .: g) c= p " B by RELAT_1:143;
A53: g c= p " (p .: g) by A49, FUNCT_1:76;
A54: p .: (p " B) = B by A3, A51, FUNCT_1:77;
p " B c= dom p by RELAT_1:132;
then p " B in GX by A5, A51, A54;
hence B = p .: g by A50, A52, A53, A54, XBOOLE_1:1; :: thesis:

end;

hence ( p .: g in X & ( for B being set st B in X & p .: g c= B holds
B = p .: g ) ) by A5, A49; :: thesis: