defpred S_{1}[ Nat] means for X being finite set st card X = $1 & X is Subset of F_{1}() & ex x being Element of F_{1}() st

( x in X & P_{1}[x] ) holds

ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) );

A2: S_{1}[ 0 ]
;

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A2, A3);

reconsider c = card F_{2}() as Nat ;

S_{1}[c]
by A40;

hence ex x being Element of F_{1}() st

( x in F_{2}() & P_{1}[x] & ( for y being Element of F_{1}() st y in F_{2}() & x <~ y holds

not P_{1}[y] ) )
by A1; :: thesis: verum

( x in X & P

ex x being Element of F

( x in X & P

not P

A2: S

A3: for k being Nat st S

S

proof

A40:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let X be finite set ; :: thesis: ( card X = k + 1 & X is Subset of F_{1}() & ex x being Element of F_{1}() st

( x in X & P_{1}[x] ) implies ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) ) )

assume that

A5: card X = k + 1 and

A6: X is Subset of F_{1}()
; :: thesis: ( for x being Element of F_{1}() holds

( not x in X or not P_{1}[x] ) or ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) ) )

given x being Element of F_{1}() such that A7:
x in X
and

A8: P_{1}[x]
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

set Xmx = X \ {x};

reconsider Xmx = X \ {x} as Subset of F_{1}() by A6, XBOOLE_1:1;

A9: card Xmx = (card X) - (card {x}) by A7, ZFMISC_1:31, CARD_2:44

.= (card X) - 1 by CARD_1:30

.= k by A5 ;

A10: Xmx \/ {x} = X by A7, ZFMISC_1:116;

end;assume A4: S

let X be finite set ; :: thesis: ( card X = k + 1 & X is Subset of F

( x in X & P

( x in X & P

not P

assume that

A5: card X = k + 1 and

A6: X is Subset of F

( not x in X or not P

( x in X & P

not P

given x being Element of F

A8: P

( x in X & P

not P

set Xmx = X \ {x};

reconsider Xmx = X \ {x} as Subset of F

A9: card Xmx = (card X) - (card {x}) by A7, ZFMISC_1:31, CARD_2:44

.= (card X) - 1 by CARD_1:30

.= k by A5 ;

A10: Xmx \/ {x} = X by A7, ZFMISC_1:116;

per cases
( ex z being Element of F_{1}() st

( z in Xmx & P_{1}[z] ) or for z being Element of F_{1}() st z in Xmx holds

not P_{1}[z] )
;

end;

( z in Xmx & P

not P

suppose
ex z being Element of F_{1}() st

( z in Xmx & P_{1}[z] )
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( z in Xmx & P

( x in X & P

not P

then consider z being Element of F_{1}() such that

A11: z in Xmx and

A12: P_{1}[z]
and

A13: for y being Element of F_{1}() st y in Xmx & y >~ z holds

not P_{1}[y]
by A4, A9;

end;A11: z in Xmx and

A12: P

A13: for y being Element of F

not P

per cases
( not x >~ z or x >~ z )
;

end;

suppose A14:
not x >~ z
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

take
z
; :: thesis: ( z in X & P_{1}[z] & ( for y being Element of F_{1}() st y in X & y >~ z holds

not P_{1}[y] ) )

thus z in X by A11; :: thesis: ( P_{1}[z] & ( for y being Element of F_{1}() st y in X & y >~ z holds

not P_{1}[y] ) )

thus P_{1}[z]
by A12; :: thesis: for y being Element of F_{1}() st y in X & y >~ z holds

not P_{1}[y]

end;not P

thus z in X by A11; :: thesis: ( P

not P

thus P

not P

suppose A17:
x >~ z
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

set Xmz = X \ {z};

reconsider Xmz = X \ {z} as Subset of F_{1}() by A6, XBOOLE_1:1;

A18: Xmz \/ {z} = X by A11, ZFMISC_1:116;

A19: card Xmz = (card X) - (card {z}) by A11, ZFMISC_1:31, CARD_2:44

.= (card X) - 1 by CARD_1:30

.= k by A5 ;

A20: x in Xmz by A7, A17, ZFMISC_1:56;

then consider v being Element of F_{1}() such that

A21: v in Xmz and

A22: P_{1}[v]
and

A23: for y being Element of F_{1}() st y in Xmz & y >~ v holds

not P_{1}[y]
by A19, A4, A8;

end;reconsider Xmz = X \ {z} as Subset of F

A18: Xmz \/ {z} = X by A11, ZFMISC_1:116;

A19: card Xmz = (card X) - (card {z}) by A11, ZFMISC_1:31, CARD_2:44

.= (card X) - 1 by CARD_1:30

.= k by A5 ;

A20: x in Xmz by A7, A17, ZFMISC_1:56;

then consider v being Element of F

A21: v in Xmz and

A22: P

A23: for y being Element of F

not P

per cases
( v = x or v <> x )
;

end;

suppose A24:
v = x
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

take
v
; :: thesis: ( v in X & P_{1}[v] & ( for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y] ) )

thus v in X by A21; :: thesis: ( P_{1}[v] & ( for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y] ) )

thus P_{1}[v]
by A22; :: thesis: for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y]

end;not P

thus v in X by A21; :: thesis: ( P

not P

thus P

not P

suppose A27:
v <> x
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

A28:
not F_{1}() is empty
by A6, A7;

not x >~ v by A20, A8, A23;

end;not x >~ v by A20, A8, A23;

per cases then
( v >~ x or v =~ x )
by A27, A28, Th27;

end;

suppose A29:
v >~ x
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

take
v
; :: thesis: ( v in X & P_{1}[v] & ( for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y] ) )

thus v in X by A21; :: thesis: ( P_{1}[v] & ( for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y] ) )

thus P_{1}[v]
by A22; :: thesis: for y being Element of F_{1}() st y in X & y >~ v holds

not P_{1}[y]

end;not P

thus v in X by A21; :: thesis: ( P

not P

thus P

not P

suppose A32:
v =~ x
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

( x in X & P

not P

take
x
; :: thesis: ( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

thus x in X by A7; :: thesis: ( P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

thus P_{1}[x]
by A8; :: thesis: for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y]

end;not P

thus x in X by A7; :: thesis: ( P

not P

thus P

not P

hereby :: thesis: verum

let y be Element of F_{1}(); :: thesis: ( y in X & y >~ x implies not P_{1}[b_{1}] )

assume that

A33: y in X and

A34: y >~ x ; :: thesis: P_{1}[b_{1}]

end;assume that

A33: y in X and

A34: y >~ x ; :: thesis: P

per cases
( y in Xmz or y in {z} )
by A18, A33, XBOOLE_0:def 3;

end;

suppose A35:
y in Xmz
; :: thesis: P_{1}[b_{1}]

y >~ v
_{1}[y]
by A35, A23; :: thesis: verum

end;proof

hence
P
assume A36:
not y >~ v
; :: thesis: contradiction

end;suppose A37:
for z being Element of F_{1}() st z in Xmx holds

not P_{1}[z]
; :: thesis: ex x being Element of F_{1}() st

( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

not P

( x in X & P

not P

take
x
; :: thesis: ( x in X & P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

thus x in X by A7; :: thesis: ( P_{1}[x] & ( for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y] ) )

thus P_{1}[x]
by A8; :: thesis: for y being Element of F_{1}() st y in X & y >~ x holds

not P_{1}[y]

end;not P

thus x in X by A7; :: thesis: ( P

not P

thus P

not P

hereby :: thesis: verum

let y be Element of F_{1}(); :: thesis: ( y in X & y >~ x implies not P_{1}[b_{1}] )

assume that

A38: y in X and

A39: y >~ x ; :: thesis: P_{1}[b_{1}]

end;assume that

A38: y in X and

A39: y >~ x ; :: thesis: P

reconsider c = card F

S

hence ex x being Element of F

( x in F

not P