theorem Th19: :: SIN_COS7:19

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