( A is non empty Subset of NAT implies ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) ) )

proof

defpred S₁[ Nat] means $1 in A;
consider x being Element of A;
assume A1: A is non empty Subset of NAT ; :: thesis: ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) )
then x is Element of NAT by TARSKI:def 3;
then A2: ex k being Nat st S₁[k] by A1;
ex k being Nat st
( S₁[k] & ( for i being Nat st S₁[i] holds
k <= i ) ) from NAT_1:sch 5(A2);
hence ex i being Nat st
( i in A & ( for k being Nat st k in A holds
i <= k ) ) ; :: thesis: verum

end;

hence ( ( A is non empty Subset of NAT implies ex b₁ being Element of NAT st
( b₁ in A & ( for k being Nat st k in A holds
b₁ <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b₁ being Element of NAT st b₁ = 0 ) ) ; :: thesis: verum