let a, b, c be Element of COMPLEX ; :: thesis: ( a <> b & a <> c & b <> c & not angle a,b,c <> 0 & not angle b,c,a <> 0 implies angle c,a,b <> 0 )
assume that
A1: a <> b and
A2: a <> c and
A3: b <> c ; :: thesis: ( angle a,b,c <> 0 or angle b,c,a <> 0 or angle c,a,b <> 0 )
assume A4: ( not angle a,b,c <> 0 & not angle b,c,a <> 0 & not angle c,a,b <> 0 ) ; :: thesis: contradiction
then A5: Arg (a - c) = Arg (b - c) by Th88;
A6: Arg (b - a) = Arg (c - a) by A4, Th88;
A7: ( a - b <> 0 & b - a <> 0 & a - c <> 0 & c - a <> 0 & b - c <> 0 & c - b <> 0 ) by A1, A2, A3;
A8: ( - (a - b) = b - a & - (b - a) = a - b ) ;
( - (a - c) = c - a & - (c - a) = a - c ) ;
then A9: Arg (a - b) = Arg (a - c) by A6, A7, A8, Th78;
( Arg (c - b) < PI iff Arg (- (c - b)) >= PI ) by A7, Th25;
hence contradiction by A4, A5, A9, Th88; :: thesis: verum