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