theorem Th13: :: SQUARE_1:13

for a being Real st 0 < a & a < 1 holds
a ^2 < a