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: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
A3: 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 that
Y <> {} and
A4: Y c= Seg (m + 1) and
A5: 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 A6: x in Y ; :: thesis: x in Seg m
then x in Seg (m + 1) by A4;
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
A7: x = j and
A8: 1 <= j and
A9: j <= m + 1 ;
j < m + 1 by A5, A6, A7, A9, XXREAL_0:1;
then j <= m by NAT_1:13;
hence x in Seg m by A7, A8, 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 that
A10: X <> {} and
A11: 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 A3, A10, A11;
then consider k being Nat such that
A12: 1 <= k and
A13: k <= m and
A14: ( k in X & ( for i being Nat st 1 <= i & i < k holds
not i in X ) ) by A2, A10;
m <= m + 1 by NAT_1:11;
then k <= m + 1 by A13, 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 A12, A14; :: thesis: verum

end;

suppose A15: 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 A16: not m + 1 in X \ {(m + 1)} by XBOOLE_0:def 5;
A17: X \ {(m + 1)} c= Seg (m + 1) by A11, XBOOLE_1:1;

now

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

suppose A18: 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 A3, A16, A17;
then consider k being Nat such that
A19: 1 <= k and
A20: k <= m and
A21: k in X \ {(m + 1)} and
A22: for i being Nat st 1 <= i & i < k holds
not i in X \ {(m + 1)} by A2, A18;
m <= m + 1 by NAT_1:11;
then A23: k <= m + 1 by A20, 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 ( 1 <= i & i < k ) ; :: thesis: not i in X
then ( not i in {(m + 1)} & not i in X \ {(m + 1)} ) by A22, A23, TARSKI:def 1;
hence not i in X by 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 A19, A21, A23; :: 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 X c= {(m + 1)} by XBOOLE_1:37;
then ( 1 <= m + 1 & ( for i being Nat st 1 <= i & i < m + 1 holds
not i in X ) ) by NAT_1:11, 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 A15; :: 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;

A24: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A24, A1);
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