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:70, XREAL_1:68;
then A1: ( PI * (- 2) <= 0 * (- 2) & ((angle (p4,p5,p6)) * 2) - (6 * PI) < (4 * PI) - (6 * PI) ) by XREAL_1:9;
assume angle (p1,p2,p3) = (2 * (angle (p4,p5,p6))) - (6 * PI) ; :: thesis: contradiction
hence contradiction by A1, COMPLEX2:70; :: thesis: verum