let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,PI.] implies sin is_orthogonal_with cos ,A )
assume A = [.0,PI.] ; :: thesis: sin is_orthogonal_with cos ,A
then |||(sin,cos,A)||| = 0 by INTEGRA8:92;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum