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:70;
A2: ( (2 * PI) * 0 <= angle (p4,p5,p6) & angle (p4,p5,p6) < (2 * PI) + ((2 * PI) * 0) ) by COMPLEX2:70;
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