let a, b, c be Element of COMPLEX ; :: thesis: ( a <> b & b <> c & angle a,b,c > PI implies ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI & angle b,c,a > PI & angle c,a,b > PI ) )
assume that
A1: ( a <> b & b <> c ) and
A2: angle a,b,c > PI ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI & angle b,c,a > PI & angle c,a,b > PI )
A3: angle c,b,a < PI

proof

assume not angle c,b,a < PI ; :: thesis: contradiction
then (angle a,b,c) + (angle c,b,a) > PI + PI by A2, XREAL_1:10;
hence contradiction by A2, Th94, COMPTRIG:21; :: thesis: verum

end;

A4: (angle a,b,c) + (angle c,b,a) = (2 * PI ) + 0 by A2, Th94, COMPTRIG:21;
then A5: angle c,b,a <> 0 by Th84;
A6: 0 <= angle c,b,a by Th84;
then angle b,a,c > 0 by A1, A5, A3, Th98;
then A7: (angle c,a,b) + (angle b,a,c) = (2 * PI ) + 0 by Th94;
angle a,c,b > 0 by A1, A6, A5, A3, Th98;
then (angle b,c,a) + (angle a,c,b) = (2 * PI ) + 0 by Th94;
then ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = (((2 * PI ) + (2 * PI )) + (2 * PI )) - (((angle c,b,a) + (angle b,a,c)) + (angle a,c,b)) by A4, A7;
hence A8: ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = ((((2 * PI ) + (2 * PI )) + PI ) + PI ) - PI by A1, A6, A5, A3, Th98
.= 5 * PI ;
:: thesis: ( angle b,c,a > PI & angle c,a,b > PI )
A9: angle a,b,c < 2 * PI by Th84;
angle b,c,a < 2 * PI by Th84;
then A10: ( ((2 * PI ) + (2 * PI )) + PI = 5 * PI & (angle a,b,c) + (angle b,c,a) < (2 * PI ) + (2 * PI ) ) by A9, XREAL_1:10;
A11: ((2 * PI ) + PI ) + (2 * PI ) = 5 * PI ;

hereby :: thesis: angle c,a,b > PI

assume angle b,c,a <= PI ; :: thesis: contradiction
then A12: (angle a,b,c) + (angle b,c,a) < (2 * PI ) + PI by A9, XREAL_1:10;
angle c,a,b < 2 * PI by Th84;
hence contradiction by A8, A11, A12, XREAL_1:10; :: thesis: verum

end;

assume angle c,a,b <= PI ; :: thesis: contradiction
hence contradiction by A8, A10, XREAL_1:10; :: thesis: verum