let A, B, C be Point of (TOP-REAL 2); :: thesis: ( ( 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; :: thesis: verum