theorem :: INTEGRA9:37

for x being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
sin is_orthogonal_with cos ,A by INTEGRA8:96;