let a, b, c be 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 & a <> c ) and
A2: b <> c ; :: thesis: ( angle (a,b,c) <> 0 or angle (b,c,a) <> 0 or angle (c,a,b) <> 0 )
A3: ( b - a <> 0 & a - c <> 0 ) by A1;
c - b <> 0 by A2;
then A4: ( Arg (c - b) < PI iff Arg (- (c - b)) >= PI ) by Th14;
A5: ( - (b - a) = a - b & - (a - c) = c - a ) ;
A6: - (c - a) = a - c ;
assume A7: ( not angle (a,b,c) <> 0 & not angle (b,c,a) <> 0 & not angle (c,a,b) <> 0 ) ; :: thesis: contradiction
then A8: Arg (a - c) = Arg (b - c) by Th72;
Arg (b - a) = Arg (c - a) by A7, Th72;
then Arg (a - b) = Arg (a - c) by A3, A5, A6, Th62;
hence contradiction by A7, A8, A4, Th72; :: thesis: verum