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