let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); not angle (p1,p2,p3) = (2 * (angle (p4,p5,p6))) + (4 * PI)
angle (p4,p5,p6) >= 0
by COMPLEX2:70;
then
( 4 * PI >= 2 * PI & ((angle (p4,p5,p6)) * 2) + (4 * PI) >= 0 + (4 * PI) )
by XREAL_1:7, XREAL_1:64;
then A1:
((angle (p4,p5,p6)) * 2) + (4 * PI) >= 2 * PI
by XXREAL_0:2;
assume
angle (p1,p2,p3) = (2 * (angle (p4,p5,p6))) + (4 * PI)
; contradiction
hence
contradiction
by A1, COMPLEX2:70; verum