let i, n be Element of NAT ; :: thesis: ( ( A is non empty Subset of NAT & i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) implies i = n ) & ( A is not non empty Subset of NAT & i = 0 & n = 0 implies i = n ) )
( A is non empty Subset of NAT & i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) implies i = n )

proof

assume that
A is non empty Subset of NAT and
A3: ( i in A & ( for k being Nat st k in A holds
i <= k ) & n in A & ( for k being Nat st k in A holds
n <= k ) ) ; :: thesis: i = n
( i <= n & n <= i ) by A3;
hence i = n by XXREAL_0:1; :: thesis: verum

end;

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