theorem Th22: :: SIN_COS7:22

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