let
x1
,
y1
be
Real
;
:: thesis:
(
x1
>=
0
&
y1
>
0
implies
x1
to_power
y1
>=
0
)
assume
that
A1
:
x1
>=
0
and
A2
:
y1
>
0
;
:: thesis:
x1
to_power
y1
>=
0
(
x1
>
0
or
x1
=
0
)
by
A1
;
hence
x1
to_power
y1
>=
0
by
A2
,
POWER:34
,
POWER:def 2
;
:: thesis:
verum