defpred S_{1}[ Nat] means for A being Subset of F_{1}() st $1 + 1 = card A holds

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

( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) );

A1: ((card F_{1}()) -' 1) + 1 =
((card F_{1}()) - 1) + 1
by Th19

.= card F_{1}()
;

A2: F_{1}() c= F_{1}()
;

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

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

then ( ((card F_{1}()) -' 1) + 1 = card F_{1}() implies ex x being Element of F_{1}() st

( x in F_{1}() & ( for y being Element of F_{1}() st y in F_{1}() holds

F_{2}(x) <= F_{2}(y) ) ) )
by A2;

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

x in F_{1}()
and

A17: for y being Element of F_{1}() st y in F_{1}() holds

F_{2}(x) <= F_{2}(y)
by A1;

take x ; :: thesis: for y being Element of F_{1}() holds F_{2}(x) <= F_{2}(y)

let y be Element of F_{1}(); :: thesis: F_{2}(x) <= F_{2}(y)

thus F_{2}(x) <= F_{2}(y)
by A17; :: thesis: verum

ex x being Element of F

( x in A & ( for y being Element of F

F

A1: ((card F

.= card F

A2: F

A3: for k being Nat st S

S

proof

A15:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

now :: thesis: for A being Subset of F_{1}() st (k + 1) + 1 = card A holds

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

( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) )

hence
Sex x being Element of F

( x in A & ( for y being Element of F

F

let A be Subset of F_{1}(); :: thesis: ( (k + 1) + 1 = card A implies ex x being Element of F_{1}() st

( b_{2} in x & ( for y being Element of F_{1}() st b_{3} in x holds

F_{2}(y) <= F_{2}(b_{3}) ) ) )

assume A5: (k + 1) + 1 = card A ; :: thesis: ex x being Element of F_{1}() st

( b_{2} in x & ( for y being Element of F_{1}() st b_{3} in x holds

F_{2}(y) <= F_{2}(b_{3}) ) )

then A6: A <> {} ;

consider x being Element of A, C being Subset of A such that

A7: A = C \/ {x} and

A8: card C = k + 1 by A5, Th23;

x in A by A6;

then reconsider x = x as Element of F_{1}() ;

reconsider C = C as Subset of F_{1}() by XBOOLE_1:1;

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

A9: z in C and

A10: for y being Element of F_{1}() st y in C holds

F_{2}(z) <= F_{2}(y)
by A4, A8;

end;( b

F

assume A5: (k + 1) + 1 = card A ; :: thesis: ex x being Element of F

( b

F

then A6: A <> {} ;

consider x being Element of A, C being Subset of A such that

A7: A = C \/ {x} and

A8: card C = k + 1 by A5, Th23;

x in A by A6;

then reconsider x = x as Element of F

reconsider C = C as Subset of F

consider z being Element of F

A9: z in C and

A10: for y being Element of F

F

per cases
( F_{2}(x) <= F_{2}(z) or F_{2}(x) > F_{2}(z) )
;

end;

suppose A11:
F_{2}(x) <= F_{2}(z)
; :: thesis: ex x being Element of F_{1}() st

( b_{2} in x & ( for y being Element of F_{1}() st b_{3} in x holds

F_{2}(y) <= F_{2}(b_{3}) ) )

( b

F

take x = x; :: thesis: ( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) )

thus x in A by A6; :: thesis: for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y)

end;F

thus x in A by A6; :: thesis: for y being Element of F

F

hereby :: thesis: verum

let y be Element of F_{1}(); :: thesis: ( y in A implies F_{2}(x) <= F_{2}(b_{1}) )

assume A12: y in A ; :: thesis: F_{2}(x) <= F_{2}(b_{1})

end;assume A12: y in A ; :: thesis: F

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

( b_{2} in z & ( for y being Element of F_{1}() st b_{3} in z holds

F_{2}(y) <= F_{2}(b_{3}) ) )

( b

F

take z = z; :: thesis: ( z in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(z) <= F_{2}(y) ) )

thus z in A by A9; :: thesis: for y being Element of F_{1}() st y in A holds

F_{2}(z) <= F_{2}(y)

end;F

thus z in A by A9; :: thesis: for y being Element of F

F

hereby :: thesis: verum

let y be Element of F_{1}(); :: thesis: ( y in A implies F_{2}(z) <= F_{2}(b_{1}) )

assume A14: y in A ; :: thesis: F_{2}(z) <= F_{2}(b_{1})

end;assume A14: y in A ; :: thesis: F

proof

for k being Nat holds S
let A be Subset of F_{1}(); :: thesis: ( 0 + 1 = card A implies ex x being Element of F_{1}() st

( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) ) )

assume 0 + 1 = card A ; :: thesis: ex x being Element of F_{1}() st

( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) )

then consider x being Element of A such that

A16: A = {x} by Th24;

reconsider x = x as Element of F_{1}() by A16, ZFMISC_1:31;

take x ; :: thesis: ( x in A & ( for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y) ) )

thus x in A by A16; :: thesis: for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y)

thus for y being Element of F_{1}() st y in A holds

F_{2}(x) <= F_{2}(y)
by A16, TARSKI:def 1; :: thesis: verum

end;( x in A & ( for y being Element of F

F

assume 0 + 1 = card A ; :: thesis: ex x being Element of F

( x in A & ( for y being Element of F

F

then consider x being Element of A such that

A16: A = {x} by Th24;

reconsider x = x as Element of F

take x ; :: thesis: ( x in A & ( for y being Element of F

F

thus x in A by A16; :: thesis: for y being Element of F

F

thus for y being Element of F

F

then ( ((card F

( x in F

F

then consider x being Element of F

x in F

A17: for y being Element of F

F

take x ; :: thesis: for y being Element of F

let y be Element of F

thus F