(sqrt 5) - 1 < 3 - 1 by Lm11, XREAL_1:9;
then A1: ((sqrt 5) - 1) / 2 < 2 / 2 by XREAL_1:74;
|.tau_bar.| = - ((1 - (sqrt 5)) / 2) by Lm13, ABSVALUE:def 1
.= ((sqrt 5) - 1) / 2 ;
hence |.tau_bar.| < 1 by A1; :: thesis: verum