3
^2
=
9 ;
then
sqrt
9
=
3
by
SQUARE_1:22
;
hence
sqrt
5
<
3
by
SQUARE_1:27
;
:: thesis:
verum