let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); :: thesis: ( sin (angle p1,p2,p3) = sin (angle p4,p5,p6) & cos (angle p1,p2,p3) = cos (angle p4,p5,p6) implies angle p1,p2,p3 = angle p4,p5,p6 )
A1: ( (2 * PI ) * 0 <= angle p1,p2,p3 & angle p1,p2,p3 < (2 * PI ) + ((2 * PI ) * 0 ) ) by COMPLEX2:84;
A2: ( (2 * PI ) * 0 <= angle p4,p5,p6 & angle p4,p5,p6 < (2 * PI ) + ((2 * PI ) * 0 ) ) by COMPLEX2:84;
assume ( sin (angle p1,p2,p3) = sin (angle p4,p5,p6) & cos (angle p1,p2,p3) = cos (angle p4,p5,p6) ) ; :: thesis: angle p1,p2,p3 = angle p4,p5,p6
hence angle p1,p2,p3 = angle p4,p5,p6 by A1, A2, SIN_COS6:61; :: thesis: verum