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