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