let
a
be
Real
;
:: thesis:
(
0
<
a
implies
0
<
sqrt
a
)
assume
A1
:
0
<
a
;
:: thesis:
0
<
sqrt
a
then
sqrt
a
<>
0
^2
by
Def2
;
hence
0
<
sqrt
a
by
A1
,
Def2
;
:: thesis:
verum