let a be Real; :: 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 Th9;
hence a |^ n >= 1 by NEWTON:10; :: thesis: verum