let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3 are_mutually_different & angle p1,p2,p3 <= PI implies ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI ) )
A1: angle p1,p2,p3 >= 0 by COMPLEX2:84;
assume A2: p1,p2,p3 are_mutually_different ; :: thesis: ( not angle p1,p2,p3 <= PI or ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI ) )
then p1 <> p3 by ZFMISC_1:def 5;
then A3: euc2cpx p1 <> euc2cpx p3 by EUCLID_3:6;
p2 <> p3 by A2, ZFMISC_1:def 5;
then A4: euc2cpx p2 <> euc2cpx p3 by EUCLID_3:6;
p1 <> p2 by A2, ZFMISC_1:def 5;
then euc2cpx p1 <> euc2cpx p2 by EUCLID_3:6;
then A5: ( ((angle p1,p2,p3) + (angle p2,p3,p1)) + (angle p3,p1,p2) = PI or ((angle p1,p2,p3) + (angle p2,p3,p1)) + (angle p3,p1,p2) = 5 * PI ) by A3, A4, COMPLEX2:102;
( angle p2,p3,p1 < 2 * PI & angle p3,p1,p2 < 2 * PI ) by COMPLEX2:84;
then A6: (angle p2,p3,p1) + (angle p3,p1,p2) < (2 * PI ) + (2 * PI ) by XREAL_1:10;
assume angle p1,p2,p3 <= PI ; :: thesis: ( angle p2,p3,p1 <= PI & angle p3,p1,p2 <= PI )
then A7: (angle p1,p2,p3) + ((angle p2,p3,p1) + (angle p3,p1,p2)) < PI + (4 * PI ) by A6, XREAL_1:10;
A8: angle p3,p1,p2 >= 0 by COMPLEX2:84;
thus angle p2,p3,p1 <= PI :: thesis: angle p3,p1,p2 <= PI

proof

assume angle p2,p3,p1 > PI ; :: thesis: contradiction
then (angle p1,p2,p3) + (angle p2,p3,p1) > 0 + PI by A1, XREAL_1:10;
hence contradiction by A5, A7, A8, XREAL_1:10; :: thesis: verum

end;

A9: angle p2,p3,p1 >= 0 by COMPLEX2:84;
thus angle p3,p1,p2 <= PI :: thesis: verum

proof

assume angle p3,p1,p2 > PI ; :: thesis: contradiction
then (angle p2,p3,p1) + (angle p3,p1,p2) > 0 + PI by A9, XREAL_1:10;
hence contradiction by A5, A7, A1, XREAL_1:10; :: thesis: verum

end;