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 that
A1: a <> b and
A2: a <> c and
A3: b <> c and
A4: 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, A2, A3, A4, Th97;

suppose A5: 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 ) )

A6: 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 A2, A3, A4, A5, A6, 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 A2, A3, 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 A2, A3, A4, Th99, COMPTRIG:21; :: thesis: verum

end;

end;

end;

end;

suppose A7: 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 ) )

A8: 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, A2, A4, A7, A8, 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, A2, 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, A2, A4, Th99, COMPTRIG:21; :: thesis: verum

end;

end;

end;

end;

end;