let a, n be Nat; :: thesis: for x being non negative Real st a |^ n < x |^ n & x |^ n < (a + 1) |^ n holds
not x is Nat
let x be non negative Real; :: thesis: ( a |^ n < x |^ n & x |^ n < (a + 1) |^ n implies not x is Nat )
assume ( a |^ n < x |^ n & x |^ n < (a + 1) |^ n ) ; :: thesis: x is not Nat
then ( a < x & x < a + 1 ) by NEWTON02:41;
hence x is not Nat by NAT_1:13; :: thesis: verum