let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); :: thesis: not angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (6 * PI )
(angle p4,p5,p6) * 2 < (2 * PI ) * 2 by COMPLEX2:84, XREAL_1:70;
then A1: ( PI * (- 2) <= 0 * (- 2) & ((angle p4,p5,p6) * 2) - (6 * PI ) < (4 * PI ) - (6 * PI ) ) by XREAL_1:11;
assume angle p1,p2,p3 = (2 * (angle p4,p5,p6)) - (6 * PI ) ; :: thesis: contradiction
hence contradiction by A1, COMPLEX2:84; :: thesis: verum