theorem :: INTEGRA9:36

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