let r be real number ; :: thesis: ( 0 <= r & r <= 2 * PI & cos r = - 1 implies r = PI )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: cos r = - 1 ; :: thesis: r = PI
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = PI + ((2 * PI ) * [\(r / (2 * PI ))/]) by A3, Th25
.= PI + ((2 * PI ) * 0 ) by A1, A3, A4, Th1, SIN_COS:82
.= PI ; :: thesis: verum