defpred S₁[ Nat] means for X being finite set st card X = $1 & X <> {} holds
ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) );
A4: S₁[ 0 ] ;
A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: for X being finite set st card X = n & X <> {} holds
ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) ; :: thesis: S₁[n + 1]
let X be finite set ; :: thesis: ( card X = n + 1 & X <> {} implies ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) )
assume that
A7: card X = n + 1 and
A8: X <> {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) )
set x = the Element of X;

A9: now :: thesis: ( X \ { the Element of X} = {} implies ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) )

assume X \ { the Element of X} = {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) )
then A10: X c= { the Element of X} by XBOOLE_1:37;
thus ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) :: thesis: verum

proof

take the Element of X ; :: thesis: ( the Element of X in X & ( for y being object st y in X & y <> the Element of X holds
not P₁[y, the Element of X] ) )
thus the Element of X in X by A8; :: thesis: for y being object st y in X & y <> the Element of X holds
not P₁[y, the Element of X]
thus for y being object st y in X & y <> the Element of X holds
not P₁[y, the Element of X] by A10, TARSKI:def 1; :: thesis: verum

end;

end;

now :: thesis: ( X \ { the Element of X} <> {} implies ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) )

assume A11: X \ { the Element of X} <> {} ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) )
{ the Element of X} c= X by A8, ZFMISC_1:31;
then A12: card (X \ { the Element of X}) = (n + 1) - (card { the Element of X}) by A7, Th43;
card { the Element of X} = 1 by CARD_1:30;
then consider y being object such that
A13: y in X \ { the Element of X} and
A14: for z being object st z in X \ { the Element of X} & z <> y holds
not P₁[z,y] by A6, A11, A12;

A15: now :: thesis: ( P₁[ the Element of X,y] implies ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) )

assume A16: P₁[ the Element of X,y] ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) )
thus ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) :: thesis: verum

proof

take the Element of X ; :: thesis: ( the Element of X in X & ( for y being object st y in X & y <> the Element of X holds
not P₁[y, the Element of X] ) )
thus the Element of X in X by A8; :: thesis: for y being object st y in X & y <> the Element of X holds
not P₁[y, the Element of X]
let z be object ; :: thesis: ( z in X & z <> the Element of X implies not P₁[z, the Element of X] )
assume that
A17: z in X and
A18: z <> the Element of X and
A19: P₁[z, the Element of X] ; :: thesis: contradiction
not z in { the Element of X} by A18, TARSKI:def 1;
then A20: z in X \ { the Element of X} by A17, XBOOLE_0:def 5;
A21: not y in { the Element of X} by A13, XBOOLE_0:def 5;
A22: z = y by A3, A14, A16, A19, A20;
y <> the Element of X by A21, TARSKI:def 1;
hence contradiction by A2, A16, A19, A22; :: thesis: verum

end;

end;

now :: thesis: ( P₁[ the Element of X,y] implies ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) )

assume A23: P₁[ the Element of X,y] ; :: thesis: ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) )
thus ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) :: thesis: verum

proof

take y ; :: thesis: ( y in X & ( for y being object st y in X & y <> y holds
not P₁[y,y] ) )
thus y in X by A13; :: thesis: for y being object st y in X & y <> y holds
not P₁[y,y]
let z be object ; :: thesis: ( z in X & z <> y implies not P₁[z,y] )
assume that
A24: z in X and
A25: z <> y ; :: thesis: P₁[z,y]
( z in { the Element of X} or not z in { the Element of X} ) ;
then ( z = the Element of X or z in X \ { the Element of X} ) by A24, TARSKI:def 1, XBOOLE_0:def 5;
hence P₁[z,y] by A14, A23, A25; :: thesis: verum

end;

end;

hence ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) by A15; :: thesis: verum

end;

hence ex x being object st
( x in X & ( for y being object st y in X & y <> x holds
not P₁[y,x] ) ) by A9; :: thesis: verum

end;

A26: for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5);
card F₁() = card F₁() ;
hence ex x being object st
( x in F₁() & ( for y being object st y in F₁() & y <> x holds
not P₁[y,x] ) ) by A1, A26; :: thesis: verum