let
a
be
Real
;
:: thesis:
(
0
<=
a
&
sqrt
a
=
0
implies
a
=
0
)
(
0
<=
a
&
sqrt
a
=
0
implies
a
=
0
^2
)
by
Def2
;
hence
(
0
<=
a
&
sqrt
a
=
0
implies
a
=
0
) ;
:: thesis:
verum