let
n
be
Nat
;
:: thesis:
for
r
,
s
being non
negative
Real
st
r
>=
s
holds
r
|^
n
>=
s
|^
n
let
r
,
s
be non
negative
Real
;
:: thesis:
(
r
>=
s
implies
r
|^
n
>=
s
|^
n
)
(
n
=
0
implies (
r
|^
n
=
1 &
s
|^
n
=
1 ) )
by
NEWTON:4
;
hence
(
r
>=
s
implies
r
|^
n
>=
s
|^
n
)
by
Th40
;
:: thesis:
verum