consider A being finite set such that
A2: P₁[A] by A1;
defpred S₁[ set , set ] means $1 c= $2;
consider Y being set such that
A3: for x being set holds
( x in Y iff ( x in bool A & P₁[x] ) ) from XBOOLE_0:sch 1();
A c= A ;
then reconsider Y = Y as non empty set by A2, A3;
Y c= bool A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in bool A )
thus ( not x in Y or x in bool A ) by A3; :: thesis: verum

end;

then reconsider Y = Y as non empty finite set ;
A4: for x, y being Element of Y st S₁[x,y] & S₁[y,x] holds
x = y by XBOOLE_0:def 10;
A5: for x, y, z being Element of Y st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by XBOOLE_1:1;
A6: for X being set st X c= Y & ( for x, y being Element of Y st x in X & y in X & not S₁[x,y] holds
S₁[y,x] ) holds
ex y being Element of Y st
for x being Element of Y st x in X holds
S₁[y,x]

proof

let X be set ; :: thesis: ( X c= Y & ( for x, y being Element of Y st x in X & y in X & not S₁[x,y] holds
S₁[y,x] ) implies ex y being Element of Y st
for x being Element of Y st x in X holds
S₁[y,x] )
assume that
A7: X c= Y and
A8: for x, y being Element of Y st x in X & y in X & not S₁[x,y] holds
S₁[y,x] ; :: thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S₁[y,x]

per cases ( X = {} or X <> {} ) ;

suppose A9: X = {} ; :: thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S₁[y,x]

consider y being Element of Y;
take y ; :: thesis: for x being Element of Y st x in X holds
S₁[y,x]
thus for x being Element of Y st x in X holds
S₁[y,x] by A9; :: thesis: verum

end;

suppose A10: X <> {} ; :: thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S₁[y,x]

consider x0 being Element of X;
x0 in X by A10;
then reconsider x0 = x0 as Element of Y by A7;
deffunc H₁( set ) -> set = card { y where y is Element of Y : ( y in X & y c< $1 ) } ;
consider f being Function such that
A11: ( dom f = X & ( for x being set st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
defpred S₂[ Nat] means ex x being Element of Y st
( x in X & $1 = f . x );
A12: for k being Nat st k <> 0 & S₂[k] holds
ex n being Nat st
( n < k & S₂[n] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₂[k] implies ex n being Nat st
( n < k & S₂[n] ) )
assume A13: k <> 0 ; :: thesis: ( not S₂[k] or ex n being Nat st
( n < k & S₂[n] ) )
given x being Element of Y such that A14: x in X and
A15: k = f . x ; :: thesis: ex n being Nat st
( n < k & S₂[n] )
set fx = { a where a is Element of Y : ( a in X & a c< x ) } ;
{ a where a is Element of Y : ( a in X & a c< x ) } c= Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { a where a is Element of Y : ( a in X & a c< x ) } or a in Y )
assume a in { a where a is Element of Y : ( a in X & a c< x ) } ; :: thesis: a in Y
then ex z being Element of Y st
( a = z & z in X & z c< x ) ;
hence a in Y ; :: thesis: verum

end;

then reconsider fx = { a where a is Element of Y : ( a in X & a c< x ) } as finite set ;
A16: k = card fx by A11, A14, A15;
set A = { z where z is Element of Y : ( z in X & z c< x ) } ;
reconsider A = { z where z is Element of Y : ( z in X & z c< x ) } as non empty set by A11, A13, A14, A15, CARD_1:47;
consider z being Element of A;
z in A ;
then consider y being Element of Y such that
A17: z = y and
A18: y in X and
A19: y c< x ;
set fx0 = { a where a is Element of Y : ( a in X & a c< y ) } ;
{ a where a is Element of Y : ( a in X & a c< y ) } c= Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { a where a is Element of Y : ( a in X & a c< y ) } or a in Y )
assume a in { a where a is Element of Y : ( a in X & a c< y ) } ; :: thesis: a in Y
then ex z being Element of Y st
( a = z & z in X & z c< y ) ;
hence a in Y ; :: thesis: verum

end;

then reconsider fx0 = { a where a is Element of Y : ( a in X & a c< y ) } as finite set ;
reconsider n = card fx0 as Element of NAT ;
take n ; :: thesis: ( n < k & S₂[n] )
for a being Element of Y holds
( not y = a or not a in X or not a c< y ) ;
then A20: not y in fx0 ;
A21: y in fx by A17;
A22: fx0 c= fx

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in fx0 or a in fx )
assume a in fx0 ; :: thesis: a in fx
then consider b being Element of Y such that
A23: a = b and
A24: b in X and
A25: b c< y ;
b c< x by A19, A25, XBOOLE_1:56;
hence a in fx by A23, A24; :: thesis: verum

end;

then card fx0 c= card fx by CARD_1:27;
then n <= k by A16, NAT_1:40;
hence n < k by A16, A22, A21, A20, PRE_POLY:8, XXREAL_0:1; :: thesis: S₂[n]
take y ; :: thesis: ( y in X & n = f . y )
thus ( y in X & n = f . y ) by A11, A18; :: thesis: verum

end;

set fx0 = { y where y is Element of Y : ( y in X & y c< x0 ) } ;
{ y where y is Element of Y : ( y in X & y c< x0 ) } c= Y

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of Y : ( y in X & y c< x0 ) } or a in Y )
assume a in { y where y is Element of Y : ( y in X & y c< x0 ) } ; :: thesis: a in Y
then ex y being Element of Y st
( a = y & y in X & y c< x0 ) ;
hence a in Y ; :: thesis: verum

end;

then reconsider fx0 = { y where y is Element of Y : ( y in X & y c< x0 ) } as finite set ;
f . x0 = card fx0 by A10, A11;
then A26: ex n being Nat st S₂[n] by A10;
S₂[ 0 ] from NAT_1:sch 7(A26, A12);
then consider y being Element of Y such that
A27: y in X and
A28: 0 = f . y ;
take y ; :: thesis: for x being Element of Y st x in X holds
S₁[y,x]
let x be Element of Y; :: thesis: ( x in X implies S₁[y,x] )
assume A29: x in X ; :: thesis: S₁[y,x]
then ( x c= y or y c= x ) by A8, A27;
then ( x c< y or y c= x ) by XBOOLE_0:def 8;
then A30: ( x in { z where z is Element of Y : ( z in X & z c< y ) } or y c= x ) by A29;
f . y = card { z where z is Element of Y : ( z in X & z c< y ) } by A11, A27;
hence S₁[y,x] by A28, A30; :: thesis: verum

end;

end;

end;

A31: for x being Element of Y holds S₁[x,x] ;
consider x being Element of Y such that
A32: for y being Element of Y st x <> y holds
not S₁[y,x] from ORDERS_1:sch 2(A31, A4, A5, A6);
x in bool A by A3;
then reconsider x = x as finite set ;
take x ; :: thesis: ( P₁[x] & ( for B being set st B c= x & P₁[B] holds
B = x ) )
thus P₁[x] by A3; :: thesis: for B being set st B c= x & P₁[B] holds
B = x
let B be set ; :: thesis: ( B c= x & P₁[B] implies B = x )
assume that
A33: B c= x and
A34: P₁[B] ; :: thesis: B = x
x in bool A by A3;
then B c= A by A33, XBOOLE_1:1;
then B in Y by A3, A34;
hence B = x by A32, A33; :: thesis: verum