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 and
A2: b <> c and
A3: 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 )
A4: (angle a,b,c) + (angle c,b,a) = (2 * PI ) + 0 by A3, Th94, COMPTRIG:21;
A5: 0 <= angle c,b,a by Th84;
A6: angle c,b,a <> 0 by A4, Th84;
A7: 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 A3, XREAL_1:10;
hence contradiction by A3, Th94, COMPTRIG:21; :: thesis: verum

end;

then angle a,c,b > 0 by A1, A2, A5, A6, Th98;
then A8: (angle b,c,a) + (angle a,c,b) = (2 * PI ) + 0 by Th94;
angle b,a,c > 0 by A1, A2, A5, A6, A7, Th98;
then (angle c,a,b) + (angle b,a,c) = (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, A8;
hence A9: ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = ((((2 * PI ) + (2 * PI )) + PI ) + PI ) - PI by A1, A2, A5, A6, A7, Th98
.= 5 * PI ;
:: thesis: ( angle b,c,a > PI & angle c,a,b > PI )
A10: ((2 * PI ) + PI ) + (2 * PI ) = 5 * PI ;
A11: ((2 * PI ) + (2 * PI )) + PI = 5 * PI ;
A12: angle a,b,c < 2 * PI by Th84;

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

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

end;

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