let r be Real; :: thesis: ( 0 <= r & r <= 2 * PI & sin r = 1 implies r = PI / 2 )
assume that
A1: 0 <= r and
A2: r <= 2 * PI and
A3: sin r = 1 ; :: thesis: r = PI / 2
A4: ( r = 2 * PI or r < 2 * PI ) by A2, XXREAL_0:1;
thus r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) by A3, Th24
.= (PI / 2) + ((2 * PI) * 0) by A1, A3, A4, Th1, SIN_COS:77
.= PI / 2 ; :: thesis: verum