let A be closed-interval Subset of REAL; :: thesis: ( A = [.0,(PI * 2).] implies sin is_orthogonal_with cos ,A )
assume A = [.0,(PI * 2).] ; :: thesis: sin is_orthogonal_with cos ,A
then |||(sin,cos,A)||| = 0 by INTEGRA8:94;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum