let n be Nat; :: thesis: for X being set st X <> {} & X c= Seg n holds
ex k being Nat st
( 1 <= k & k <= n & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )
let X be set ; :: thesis: ( X <> {} & X c= Seg n implies ex k being Nat st
( 1 <= k & k <= n & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) )
defpred S₁[ Nat] means for X being set st X <> {} & X c= Seg $1 holds
ex k being Nat st
( 1 <= k & k <= $1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) );
A1: S₁[ 0 ] ;
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
B2: for Y being set st Y <> {} & Y c= Seg (m + 1) & not m + 1 in Y holds
Y c= Seg m

proof

let Y be set ; :: thesis: ( Y <> {} & Y c= Seg (m + 1) & not m + 1 in Y implies Y c= Seg m )
assume D1: ( Y <> {} & Y c= Seg (m + 1) & not m + 1 in Y ) ; :: thesis: Y c= Seg m
Y c= Seg m

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Seg m )
assume E1: x in Y ; :: thesis: x in Seg m
then x in Seg (m + 1) by D1;
then x in { j where j is Element of NAT : ( 1 <= j & j <= m + 1 ) } by FINSEQ_1:def 1;
then consider j being Element of NAT such that
E2: ( x = j & 1 <= j & j <= m + 1 ) ;
j < m + 1 by E1, E2, D1, XXREAL_0:1;
then j <= m by NAT_1:13;
hence x in Seg m by E2, FINSEQ_1:3; :: thesis: verum

end;

hence Y c= Seg m ; :: thesis: verum

end;

for X being set st X <> {} & X c= Seg (m + 1) holds
ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

proof

let X be set ; :: thesis: ( X <> {} & X c= Seg (m + 1) implies ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) )
assume C1: ( X <> {} & X c= Seg (m + 1) ) ; :: thesis: ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

now

per cases ( not m + 1 in X or m + 1 in X ) ;

suppose not m + 1 in X ; :: thesis: ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

then X c= Seg m by C1, B2;
then consider k being Nat such that
D1: ( 1 <= k & k <= m & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) by C1, B1;
m <= m + 1 by NAT_1:11;
then k <= m + 1 by D1, XXREAL_0:2;
hence ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) by D1; :: thesis: verum

end;

suppose C3: m + 1 in X ; :: thesis: ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

set X1 = X \ {(m + 1)};
m + 1 in {(m + 1)} by TARSKI:def 1;
then D1: not m + 1 in X \ {(m + 1)} by XBOOLE_0:def 5;
D2: X \ {(m + 1)} c= Seg (m + 1) by C1, XBOOLE_1:1;

now

per cases ( X \ {(m + 1)} <> {} or X \ {(m + 1)} = {} ) ;

suppose D3: X \ {(m + 1)} <> {} ; :: thesis: ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

then X \ {(m + 1)} c= Seg m by B2, D1, D2;
then consider k being Nat such that
E1: ( 1 <= k & k <= m & k in X \ {(m + 1)} & ( for i being Nat st 1 <= i & i < k holds
not i in X \ {(m + 1)} ) ) by D3, B1;
m <= m + 1 by NAT_1:11;
then E2: k <= m + 1 by E1, XXREAL_0:2;
for i being Nat st 1 <= i & i < k holds
not i in X

proof

let i be Nat; :: thesis: ( 1 <= i & i < k implies not i in X )
assume F1: ( 1 <= i & i < k ) ; :: thesis: not i in X
F2: not i in {(m + 1)} by E2, F1, TARSKI:def 1;
not i in X \ {(m + 1)} by E1, F1;
hence not i in X by F2, XBOOLE_0:def 5; :: thesis: verum

end;

hence ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) by E1, E2; :: thesis: verum

end;

suppose X \ {(m + 1)} = {} ; :: thesis: ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) )

then E1: X c= {(m + 1)} by XBOOLE_1:37;
E2: ( 1 <= m + 1 & m + 1 <= m + 1 & m + 1 in X ) by C3, NAT_1:11;
for i being Nat st 1 <= i & i < m + 1 holds
not i in X by E1, TARSKI:def 1;
hence ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) by E2; :: thesis: verum

end;

end;

end;

hence ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) ; :: thesis: verum

end;

end;

end;

hence ex k being Nat st
( 1 <= k & k <= m + 1 & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) ; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A2);
hence ( X <> {} & X c= Seg n implies ex k being Nat st
( 1 <= k & k <= n & k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) ) ; :: thesis: verum