let r be Real; :: thesis: ( - 1 <= r & r <= 1 & arctan r = PI / 4 implies r = 1 )
assume that
A1: - 1 <= r and
A2: r <= 1 and
A3: arctan r = PI / 4 ; :: thesis: r = 1
thus r = tan (PI / 4) by A1, A2, A3, Th51
.= tan . (PI / 4) by Lm8, Th13
.= 1 by SIN_COS:def 28 ; :: thesis: verum