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