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: c - b <> 0 by A2;
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: c + (- b) <> a + (- b) by A3, Th93;
A8: 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, A7, A5, Th92 ;
A9: angle (a + (- b)),0c ,(c + (- b)) = angle (a + (- b)),(b + (- b)),(c + (- b))
.= angle a,b,c by Th86 ;
A10: a - b <> 0 by A1;
then A11: angle (a + (- b)),0c ,(c + (- b)) = angle (Rotate (a + (- b)),(- (Arg (a + (- b))))),0c ,(Rotate (c + (- b)),(- (Arg (a + (- b))))) by A6, A5, Th92;
a + (- b) <> 0c by A1;
then |.(a + (- b)).| > 0 by COMPLEX1:133;
then A12: ( Im (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0 & Re (Rotate (a + (- b)),(- (Arg (a + (- b))))) > 0 ) by COMPLEX1:28, SIN_COS:34;
then A13: Arg (Rotate (a + (- b)),(- (Arg (a + (- b))))) = 0c by Th34;
then (Arg ((Rotate (c + (- b)),(- (Arg (a + (- b))))) - 0c )) - (Arg ((Rotate (a + (- b)),(- (Arg (a + (- b))))) - 0c )) >= 0 by COMPTRIG:52;
then A14: angle a,b,c = Arg (Rotate (c + (- b)),(- (Arg (a + (- b))))) by A9, A11, A13, Def6;
A15: 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, A10, A7, Th92 ;
hence ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI by A3, A4, A9, A11, A12, A14, A8, Lm5; :: thesis: ( 0 < angle b,c,a & 0 < angle c,a,b )
thus 0 < angle b,c,a by A3, A4, A12, A14, A8, Lm5; :: thesis: 0 < angle c,a,b
thus 0 < angle c,a,b by A3, A4, A12, A14, A15, Lm5; :: thesis: verum