theorem :: INTEGRA9:35

for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds
sin is_orthogonal_with cos ,A by INTEGRA8:94;