theorem Th28: :: SIN_COS6:28

for r being Real st 0 <= r & r <= 2 * PI & sin r = 1 holds
r = PI / 2