let a be Real; :: thesis: ( 1 < a implies a < a ^2 )
assume 1 < a ; :: thesis: a < a ^2
then a * 1 < a * a by XREAL_1:68;
hence a < a ^2 ; :: thesis: verum