let a, b, c be Element of COMPLEX ; :: thesis: ( a <> b & a <> c & b <> c & angle a,b,c = 0 & not ( angle b,c,a = 0 & angle c,a,b = PI ) implies ( angle b,c,a = PI & angle c,a,b = 0 ) )
assume A1: ( a <> b & a <> c & b <> c & angle a,b,c = 0 ) ; :: thesis: ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) )

per cases ( angle b,c,a <> 0 or angle c,a,b <> 0 ) by A1, Th97;

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

A3: 0 <= angle b,c,a by Th84;
thus ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) :: thesis: verum

proof

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

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, A2, A3, Th98; :: thesis: verum

end;

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, Th100; :: thesis: verum

end;

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, Th99, COMPTRIG:21; :: thesis: verum

end;

end;

end;

end;

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

A5: 0 <= angle c,a,b by Th84;
thus ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) :: thesis: verum

proof

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

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, A4, A5, Th98; :: thesis: verum

end;

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, Th100; :: thesis: verum

end;

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

hence ( ( angle b,c,a = 0 & angle c,a,b = PI ) or ( angle b,c,a = PI & angle c,a,b = 0 ) ) by A1, Th99, COMPTRIG:21; :: thesis: verum

end;

end;

end;

end;

end;