theorem :: SIN_COS7:14

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