theorem :: SIN_COS7:3

for x being Real holds (x / (sqrt ((x ^2) + 1))) ^2 < 1