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