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:77
.= PI ; :: thesis: verum