defpred S2[ Element of NAT ] means for X being finite set st card X = $1 & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) );
A4: S2[ 0 ] ;
A5: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A6: for X being finite set st card X = n & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) ; :: thesis: S2[n + 1]
let X be finite set ; :: thesis: ( card X = n + 1 & X <> {} implies ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) )
assume that
A7: card X = n + 1 and
A8: X <> {} ; :: thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
consider x being Element of X;
A9: now
assume X \ {x} = {} ; :: thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
then A10: X c= {x} by XBOOLE_1:37;
thus ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) :: thesis: verum
proof
take x ; :: thesis: ( x in X & ( for y being set st y in X holds
P1[x,y] ) )
thus x in X by A8; :: thesis: for y being set st y in X holds
P1[x,y]
let y be set ; :: thesis: ( y in X implies P1[x,y] )
assume y in X ; :: thesis: P1[x,y]
then y = x by A10, TARSKI:def 1;
hence P1[x,y] by A2; :: thesis: verum
end;
end;
now
assume A11: X \ {x} <> {} ; :: thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
{x} c= X by A8, ZFMISC_1:37;
then A12: card (X \ {x}) = (n + 1) - (card {x}) by A7, CARD_2:63;
card {x} = 1 by CARD_1:50;
then consider y being set such that
A13: y in X \ {x} and
A14: for z being set st z in X \ {x} holds
P1[y,z] by A6, A11, A12;
A15: ( P1[x,y] or P1[y,x] ) by A2;
A16: P1[x,x] by A2;
P1[y,y] by A2;
then consider z being set such that
A17: ( z = x or z = y ) and
A18: P1[z,x] and
A19: P1[z,y] by A15, A16;
thus ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) :: thesis: verum
proof
take z ; :: thesis: ( z in X & ( for y being set st y in X holds
P1[z,y] ) )
thus z in X by A13, A17; :: thesis: for y being set st y in X holds
P1[z,y]
let u be set ; :: thesis: ( u in X implies P1[z,u] )
A20: ( u in {x} or not u in {x} ) ;
assume u in X ; :: thesis: P1[z,u]
then ( u = x or u in X \ {x} ) by A20, TARSKI:def 1, XBOOLE_0:def 5;
then ( P1[z,u] or P1[y,u] ) by A14, A18;
hence P1[z,u] by A3, A19; :: thesis: verum
end;
end;
hence ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) by A9; :: thesis: verum
end;
A21: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A4, A5);
 card F1() = card F1() ;
hence ex x being set st
( x in F1() & ( for y being set st y in F1() holds
P1[x,y] ) ) by A1, A21; :: thesis: verum