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

assume 1 < a ; :: thesis: a < a ^2

then a * 1 < a * a by XREAL_1:68;

hence a < a ^2 ; :: thesis: verum