defpred S1[ Nat] means for X being finite set st card X = \$1 & X is Subset of F1() & ex x being Element of F1() st
( x in X & P1[x] ) holds
ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) );
A2: S1[ 0 ] ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
let X be finite set ; :: thesis: ( card X = k + 1 & X is Subset of F1() & ex x being Element of F1() st
( x in X & P1[x] ) implies ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) ) )

assume that
A5: card X = k + 1 and
A6: X is Subset of F1() ; :: thesis: ( for x being Element of F1() holds
( not x in X or not P1[x] ) or ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) ) )

given x being Element of F1() such that A7: x in X and
A8: P1[x] ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

set Xmx = X \ {x};
reconsider Xmx = X \ {x} as Subset of F1() by ;
A9: card Xmx = (card X) - () by
.= (card X) - 1 by CARD_1:30
.= k by A5 ;
A10: Xmx \/ {x} = X by ;
per cases ( ex z being Element of F1() st
( z in Xmx & P1[z] ) or for z being Element of F1() st z in Xmx holds
not P1[z] )
;
suppose ex z being Element of F1() st
( z in Xmx & P1[z] ) ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

then consider z being Element of F1() such that
A11: z in Xmx and
A12: P1[z] and
A13: for y being Element of F1() st y in Xmx & y <~ z holds
not P1[y] by A4, A9;
per cases ( not x <~ z or x <~ z ) ;
suppose A14: not x <~ z ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

take z ; :: thesis: ( z in X & P1[z] & ( for y being Element of F1() st y in X & y <~ z holds
not P1[y] ) )

thus z in X by A11; :: thesis: ( P1[z] & ( for y being Element of F1() st y in X & y <~ z holds
not P1[y] ) )

thus P1[z] by A12; :: thesis: for y being Element of F1() st y in X & y <~ z holds
not P1[y]

hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in X & y <~ z implies not P1[b1] )
assume that
A15: y in X and
A16: y <~ z ; :: thesis: P1[b1]
end;
end;
suppose A17: x <~ z ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

set Xmz = X \ {z};
reconsider Xmz = X \ {z} as Subset of F1() by ;
A18: Xmz \/ {z} = X by ;
A19: card Xmz = (card X) - () by
.= (card X) - 1 by CARD_1:30
.= k by A5 ;
A20: x in Xmz by ;
then consider v being Element of F1() such that
A21: v in Xmz and
A22: P1[v] and
A23: for y being Element of F1() st y in Xmz & y <~ v holds
not P1[y] by A19, A4, A8;
per cases ( v = x or v <> x ) ;
suppose A24: v = x ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

take v ; :: thesis: ( v in X & P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )

thus v in X by A21; :: thesis: ( P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )

thus P1[v] by A22; :: thesis: for y being Element of F1() st y in X & y <~ v holds
not P1[y]

hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in X & y <~ v implies not P1[b1] )
assume that
A25: y in X and
A26: y <~ v ; :: thesis: P1[b1]
end;
end;
suppose A27: v <> x ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

A28: not F1() is empty by A6, A7;
not x <~ v by A20, A8, A23;
per cases then ( v <~ x or v =~ x ) by ;
suppose A29: v <~ x ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

take v ; :: thesis: ( v in X & P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )

thus v in X by A21; :: thesis: ( P1[v] & ( for y being Element of F1() st y in X & y <~ v holds
not P1[y] ) )

thus P1[v] by A22; :: thesis: for y being Element of F1() st y in X & y <~ v holds
not P1[y]

hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in X & y <~ v implies not P1[b1] )
assume that
A30: y in X and
A31: y <~ v ; :: thesis: P1[b1]
end;
end;
suppose A32: v =~ x ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

take x ; :: thesis: ( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

thus x in X by A7; :: thesis: ( P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

thus P1[x] by A8; :: thesis: for y being Element of F1() st y in X & y <~ x holds
not P1[y]

hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in X & y <~ x implies not P1[b1] )
assume that
A33: y in X and
A34: y <~ x ; :: thesis: P1[b1]
per cases ( y in Xmz or y in {z} ) by ;
end;
end;
end;
end;
end;
end;
end;
end;
end;
suppose A37: for z being Element of F1() st z in Xmx holds
not P1[z] ; :: thesis: ex x being Element of F1() st
( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

take x ; :: thesis: ( x in X & P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

thus x in X by A7; :: thesis: ( P1[x] & ( for y being Element of F1() st y in X & y <~ x holds
not P1[y] ) )

thus P1[x] by A8; :: thesis: for y being Element of F1() st y in X & y <~ x holds
not P1[y]

hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in X & y <~ x implies not P1[b1] )
assume that
A38: y in X and
A39: y <~ x ; :: thesis: P1[b1]
end;
end;
end;
end;
A40: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
reconsider c = card F2() as Nat ;
S1[c] by A40;
hence ex x being Element of F1() st
( x in F2() & P1[x] & ( for y being Element of F1() st y in F2() & y <~ x holds
not P1[y] ) ) by A1; :: thesis: verum