let A be 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