let x be real number ; :: thesis: ( 0 < x & x < 1 implies x ^2 < 1 )
assume A1: ( 0 < x & x < 1 ) ; :: thesis: x ^2 < 1
then x ^2 < x by SQUARE_1:75;
hence x ^2 < 1 by A1, XXREAL_0:2; :: thesis: verum