( 21 ^2 < 464 & 464 < (21 + 1) ^2 ) ;
hence for i being Integer holds not i ^2 = 464 by Th105; :: thesis: verum