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 & y <> x holds
not P1[y,x] ) );
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 & y <> x holds
not P1[y,x] ) ) ; :: 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 & y <> x holds
not P1[y,x] ) ) )
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 & y <> x holds
not P1[y,x] ) )
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 & y <> x holds
not P1[y,x] ) )
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 & y <> x holds
not P1[y,x] ) ) :: thesis: verum
proof
take x ; :: thesis: ( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus x in X by A8; :: thesis: for y being set st y in X & y <> x holds
not P1[y,x]
thus for y being set st y in X & y <> x holds
not P1[y,x] by A10, TARSKI:def 1; :: 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 & y <> x holds
not P1[y,x] ) )
{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} & z <> y holds
not P1[z,y] by A6, A11, A12;
A15: now
assume A16: P1[x,y] ; :: thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) :: thesis: verum
proof
take x ; :: thesis: ( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus x in X by A8; :: thesis: for y being set st y in X & y <> x holds
not P1[y,x]
let z be set ; :: thesis: ( z in X & z <> x implies not P1[z,x] )
assume that
A17: z in X and
A18: z <> x and
A19: P1[z,x] ; :: thesis: contradiction
not z in {x} by A18, TARSKI:def 1;
then A20: z in X \ {x} by A17, XBOOLE_0:def 5;
A21: not y in {x} by A13, XBOOLE_0:def 5;
A22: z = y by A3, A14, A16, A19, A20;
y <> x by A21, TARSKI:def 1;
hence contradiction by A2, A16, A19, A22; :: thesis: verum
end;
end;
now
assume A23: P1[x,y] ; :: thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) :: thesis: verum
proof
take y ; :: thesis: ( y in X & ( for y being set st y in X & y <> y holds
not P1[y,y] ) )
thus y in X by A13; :: thesis: for y being set st y in X & y <> y holds
not P1[y,y]
let z be set ; :: thesis: ( z in X & z <> y implies not P1[z,y] )
assume that
A24: z in X and
A25: z <> y ; :: thesis: P1[z,y]
( z in {x} or not z in {x} ) ;
then ( z = x or z in X \ {x} ) by A24, TARSKI:def 1, XBOOLE_0:def 5;
hence P1[z,y] by A14, A23, A25; :: thesis: verum
end;
end;
hence ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) by A15; :: thesis: verum
end;
hence ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) by A9; :: thesis: verum
end;
A26: 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() & y <> x holds
not P1[y,x] ) ) by A1, A26; :: thesis: verum