theorem :: SIN_COS7:16

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