let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1,p2,p3 are_mutually_distinct & angle (p1,p2,p3) <= PI implies ( angle (p2,p3,p1) <= PI & angle (p3,p1,p2) <= PI ) )
A1: angle (p1,p2,p3) >= 0 by COMPLEX2:70;
assume A2: p1,p2,p3 are_mutually_distinct ; :: 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:4;
p2 <> p3 by A2, ZFMISC_1:def 5;
then A4: euc2cpx p2 <> euc2cpx p3 by EUCLID_3:4;
p1 <> p2 by A2, ZFMISC_1:def 5;
then euc2cpx p1 <> euc2cpx p2 by EUCLID_3:4;
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:88;
( angle (p2,p3,p1) < 2 * PI & angle (p3,p1,p2) < 2 * PI ) by COMPLEX2:70;
then A6: (angle (p2,p3,p1)) + (angle (p3,p1,p2)) < (2 * PI) + (2 * PI) by XREAL_1:8;
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:8;
A8: angle (p3,p1,p2) >= 0 by COMPLEX2:70;
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:8;
hence contradiction by A5, A7, A8, XREAL_1:8; :: thesis: verum
end;
A9: angle (p2,p3,p1) >= 0 by COMPLEX2:70;
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:8;
hence contradiction by A5, A7, A1, XREAL_1:8; :: thesis: verum
end;