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