let A, B, C be Point of (TOP-REAL 2); ( ( 0 <= angle (A,B,C) & angle (A,B,C) < PI ) or angle (A,B,C) = PI or ( PI < angle (A,B,C) & angle (A,B,C) < 2 * PI ) )
set alpha = angle (A,B,C);
( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI )
by Th2;
then
angle (A,B,C) in ([.0,PI.[ \/ {PI}) \/ ].PI,(2 * PI).[
by Lm1, XXREAL_1:3;
then
( angle (A,B,C) in [.0,PI.[ \/ {PI} or angle (A,B,C) in ].PI,(2 * PI).[ )
by XBOOLE_0:def 3;
then
( angle (A,B,C) in [.0,PI.[ or angle (A,B,C) in {PI} or angle (A,B,C) in ].PI,(2 * PI).[ )
by XBOOLE_0:def 3;
hence
( ( 0 <= angle (A,B,C) & angle (A,B,C) < PI ) or angle (A,B,C) = PI or ( PI < angle (A,B,C) & angle (A,B,C) < 2 * PI ) )
by XXREAL_1:3, TARSKI:def 1, XXREAL_1:4; verum