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:5; :: 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:5; :: thesis: verum

end;

end;

end;

end;

end;