let a be real number ; :: thesis: for n being natural number st a >= 1 holds
a |^ n >= 1
let n be natural number ; :: thesis: ( a >= 1 implies a |^ n >= 1 )
assume a >= 1 ; :: thesis: a |^ n >= 1
then a |^ n >= 1 |^ n by Th17;
hence a |^ n >= 1 by NEWTON:15; :: thesis: verum