let r be Real; :: thesis: ( - 1 <= r & r <= 1 & arctan r = PI / 4 implies r = 1 )
assume ( - 1 <= r & r <= 1 & arctan r = PI / 4 ) ; :: thesis: r = 1
hence r = tan (PI / 4) by Th49
.= tan . (PI / 4) by Lm8, Th13
.= 1 by SIN_COS:def 32 ;
:: thesis: verum