let a, b, c be Element of COMPLEX ; :: thesis: ( a <> b & b <> c & 0 < angle a,b,c & angle a,b,c < PI implies ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI & 0 < angle b,c,a & 0 < angle c,a,b ) )
assume that
A1: a <> b and
A2: b <> c and
A3: 0 < angle a,b,c and
A4: angle a,b,c < PI ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI & 0 < angle b,c,a & 0 < angle c,a,b )
A5: angle (a + (- b)),0c ,(c + (- b)) = angle (a + (- b)),(b + (- b)),(c + (- b))
.= angle a,b,c by Th86 ;
set r = - (Arg (a + (- b)));
set A = Rotate (a + (- b)),(- (Arg (a + (- b))));
set B = Rotate (c + (- b)),(- (Arg (a + (- b))));
A6: Rotate 0c ,(- (Arg (a + (- b)))) = 0c by Th66;
A7: a - b <> 0 by A1;
A8: c + (- b) <> a + (- b) by A3, Th93;
A9: c - b <> 0 by A2;
then A10: angle (a + (- b)),0c ,(c + (- b)) = angle (Rotate (a + (- b)),(- (Arg (a + (- b))))),0c ,(Rotate (c + (- b)),(- (Arg (a + (- b))))) by A6, A7, Th92;
A12: Im (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0 by COMPLEX1:28, SIN_COS:34;
a + (- b) <> 0c by A1;
then |.(a + (- b)).| > 0 by COMPLEX1:133;
then A13: Re (Rotate (a + (- b)),(- (Arg (a + (- b))))) > 0 by SIN_COS:34, COMPLEX1:28;
then A14: Arg (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0c by A12, Th34;
then (Arg ((Rotate (c + (- b)),(- (Arg (a + (- b))))) - 0c )) - (Arg ((Rotate (a + (- b)),(- (Arg (a + (- b))))) - 0c )) >= 0 by COMPTRIG:52;
then A15: angle a,b,c = Arg (Rotate (c + (- b)),(- (Arg (a + (- b))))) by A5, A10, A14, Def6;
A16: angle b,c,a = angle (b + (- b)),(c + (- b)),(a + (- b)) by Th86
.= angle 0c ,(Rotate (c + (- b)),(- (Arg (a + (- b))))),(Rotate (a + (- b)),(- (Arg (a + (- b))))) by A6, A8, A9, Th92 ;
A17: angle c,a,b = angle (c + (- b)),(a + (- b)),(b + (- b)) by Th86
.= angle (Rotate (c + (- b)),(- (Arg (a + (- b))))),(Rotate (a + (- b)),(- (Arg (a + (- b))))),0c by A6, A7, A8, Th92 ;
hence ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI by A3, A4, A5, A10, A12, A13, A15, A16, Lm6; :: thesis: ( 0 < angle b,c,a & 0 < angle c,a,b )
thus 0 < angle b,c,a by A3, A4, A12, A13, A15, A16, Lm6; :: thesis: 0 < angle c,a,b
thus 0 < angle c,a,b by A3, A4, A12, A13, A15, A17, Lm6; :: thesis: verum