let a, b, c be Element of COMPLEX ; :: thesis: ( ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) iff ( a <> b & a <> c & b <> c ) )

hereby :: thesis: ( a <> b & a <> c & b <> c & not ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI implies ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

assume A1: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) ; :: thesis: ( a <> b & a <> c & b <> c )

per cases ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) by A1;

suppose A2: ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI ; :: thesis: ( a <> b & a <> c & b <> c )

thus ( a <> b & a <> c & b <> c ) :: thesis: verum

proof

assume A3: ( not a <> b or not a <> c or not b <> c ) ; :: thesis: contradiction

per cases ( a = b or a = c or b = c ) by A3;

suppose A4: a = b ; :: thesis: contradiction

A5: angle a,c,a = 0 by Th93;
( not angle a,a,c = 0 or not angle c,a,a = 0 ) by A2, A4, Th93, COMPTRIG:21;
hence contradiction by A2, A4, A5, Th94, COMPTRIG:21; :: thesis: verum

end;

suppose A6: a = c ; :: thesis: contradiction

A7: angle a,b,a = 0 by Th93;
( not angle a,a,b = 0 or not angle b,a,a = 0 ) by A2, A6, Th93, COMPTRIG:21;
hence contradiction by A2, A6, A7, Th94, COMPTRIG:21; :: thesis: verum

end;

suppose A8: b = c ; :: thesis: contradiction

A9: angle b,a,b = 0 by Th93;
( not angle a,b,b = 0 or not angle b,b,a = 0 ) by A2, A8, Th93, COMPTRIG:21;
hence contradiction by A2, A8, A9, Th94, COMPTRIG:21; :: thesis: verum

end;

end;

end;

end;

suppose A10: ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ; :: thesis: ( a <> b & a <> c & b <> c )

A11: (2 + 2) * PI < 5 * PI by COMPTRIG:21, XREAL_1:70;
then A12: (2 * PI ) + (2 * PI ) < 5 * PI ;
thus ( a <> b & a <> c & b <> c ) :: thesis: verum

proof

assume A13: ( not a <> b or not a <> c or not b <> c ) ; :: thesis: contradiction

per cases ( a = b or b = c or a = c ) by A13;

suppose a = b ; :: thesis: contradiction

then angle b,c,a = 0 by Th93;
then A14: (angle a,b,c) + (angle b,c,a) < 2 * PI by Th84;
angle c,a,b < 2 * PI by Th84;
hence contradiction by A10, A12, A14, XREAL_1:10; :: thesis: verum

end;

suppose A15: b = c ; :: thesis: contradiction

( angle a,b,c < 2 * PI & angle b,c,a < 2 * PI ) by Th84;
then A16: (angle a,b,c) + (angle b,c,a) < (2 * PI ) + (2 * PI ) by XREAL_1:10;
angle c,a,b = 0 by A15, Th93;
hence contradiction by A10, A11, A16; :: thesis: verum

end;

suppose a = c ; :: thesis: contradiction

then angle a,b,c = 0 by Th93;
then A17: (angle a,b,c) + (angle b,c,a) < 2 * PI by Th84;
angle c,a,b < 2 * PI by Th84;
hence contradiction by A10, A12, A17, XREAL_1:10; :: thesis: verum

end;

end;

end;

end;

end;

end;

assume that
A18: a <> b and
A19: a <> c and
A20: b <> c ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

per cases ( angle a,b,c = 0 or ( 0 <> angle a,b,c & angle a,b,c < PI ) or ( 0 <> angle a,b,c & angle a,b,c = PI ) or ( 0 <> angle a,b,c & angle a,b,c > PI ) ) by XXREAL_0:1;

suppose A21: angle a,b,c = 0 ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

(angle b,c,a) + (angle c,a,b) = PI

proof

per cases ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A18, A19, A20, A21, Th101;

suppose ( angle b,c,a = 0 & angle c,a,b = PI ) ; :: thesis: (angle b,c,a) + (angle c,a,b) = PI

hence (angle b,c,a) + (angle c,a,b) = PI ; :: thesis: verum

end;

suppose ( angle b,c,a = PI & angle c,a,b = 0 ) ; :: thesis: (angle b,c,a) + (angle c,a,b) = PI

hence (angle b,c,a) + (angle c,a,b) = PI ; :: thesis: verum

end;

end;

end;

hence ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) by A21; :: thesis: verum

end;

suppose A22: ( 0 <> angle a,b,c & angle a,b,c < PI ) ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

0 <= angle a,b,c by Th84;
hence ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) by A18, A20, A22, Th98; :: thesis: verum

end;

suppose A23: ( 0 <> angle a,b,c & angle a,b,c = PI ) ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

then angle b,c,a = 0 by A18, A20, Th100;
hence ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) by A18, A20, A23, Th100; :: thesis: verum

end;

suppose ( 0 <> angle a,b,c & angle a,b,c > PI ) ; :: thesis: ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI )

hence ( ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = PI or ((angle a,b,c) + (angle b,c,a)) + (angle c,a,b) = 5 * PI ) by A18, A20, Th99; :: thesis: verum

end;

end;