let a be Real; :: thesis: ( 0 < a & a < 1 implies a ^2 < a )
assume that
A1: 0 < a and
A2: a < 1 ; :: thesis: a ^2 < a
a * a < a * 1 by A1, A2, XREAL_1:68;
hence a ^2 < a ; :: thesis: verum