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;
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 XFAMILY:sch 1();
G c= bool (dom p) by A5;
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₂[ 0 ]

assume 0 in omega ; :: thesis:
let X be Subset-Family of 0; :: 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 XFAMILY:sch 1();
X1 c= bool O by A14;
then reconsider X2 = X1 as Subset-Family of O ;
set y = the Element of X;
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 XBOOLE_1:33;
then A15: the Element of X \ {O} c= O \ {O} by XBOOLE_1:40;
A16: O in succ O by ORDINAL1:6;
A17: not O in O ;
then the Element of X \ {O} c= O by A15, ZFMISC_1:57;
then X2 <> {} by A13, A14;
then consider Z being set such that
A18: Z in X2 and
A19: for B being set st B in X2 & Z c= B holds
B = Z by A11, A12, A16;
consider X1 being set such that
A20: X1 in X and
A21: Z = X1 \ {O} by A14, A18;
A22: O in {O} by TARSKI:def 1;
then A23: not O in Z by A21, XBOOLE_0:def 5;

A24: now :: thesis:

assume A25: 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 A26: B in X ; :: thesis:
assume A27: A c= B ; :: thesis:

A28: now :: thesis:

assume A29: O in B ; :: thesis:
set Y = B \ {O};
{O} c= B by A29, ZFMISC_1:31;
then A30: B = (B \ {O}) \/ {O} by XBOOLE_1:45;
A \ {O} c= B \ {O} by A27, XBOOLE_1:33;
then A31: Z \ {O} c= B \ {O} by XBOOLE_1:40;
not O in Z by A21, A22, XBOOLE_0:def 5;
then A32: Z c= B \ {O} by A31, ZFMISC_1:57;
B \ {O} c= (O \/ {O}) \ {O} by A26, XBOOLE_1:33;
then B \ {O} c= O \ {O} by XBOOLE_1:40;
then B \ {O} c= O by A17, ZFMISC_1:57;
then B \ {O} in X2 by A14, A26;
hence B = A by A19, A30, A32; :: thesis:

end;

now :: thesis:

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

end;

hence B = A by A28; :: 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;

now :: thesis:

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

now :: thesis:

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

end;

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

proof

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

A40: now :: thesis:

assume A41: O in B ; :: thesis:
A \/ {O} = (B \ {O}) \/ {O} by A19, A37, A39
.= B \/ {O} by XBOOLE_1:39
.= B by A41, ZFMISC_1:40 ;
hence contradiction by A34, A36; :: thesis:

end;

A42: B c= O

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A43: x in B ; :: thesis:
( x in O or x in {O} ) by A36, A43, XBOOLE_0:def 3;
hence x in O by A40, A43, TARSKI:def 1; :: thesis:

end;

B \ {O} = B by A40, ZFMISC_1:57;
then B in X2 by A14, A36, A42;
hence B = A by A19, A38; :: 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 A35; :: 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 A24; :: thesis:

end;

A44: for O being Ordinal st O <> 0 & 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
A45: O <> 0 and
A46: O is limit_ordinal and
for B being Ordinal st B in O holds
S₂[B] and
A47: O in omega ; :: thesis:
{} in O by A45, ORDINAL1:14;
then omega c= O by A46, ORDINAL1:def 11;
then O in O by A47;
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, A44);
then consider g being set such that
A48: g in GX and
A49: 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 A50: B in X ; :: thesis:
assume p .: g c= B ; :: thesis:
then A51: p " (p .: g) c= p " B by RELAT_1:143;
A52: g c= p " (p .: g) by A48, FUNCT_1:76;
A53: p .: (p " B) = B by A3, A50, FUNCT_1:77;
p " B c= dom p by RELAT_1:132;
then p " B in GX by A5, A50, A53;
hence B = p .: g by A49, A51, A52, A53, 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, A48; :: thesis: