sqrt 5 < sqrt (3 ^2) by SQUARE_1:27;
then sqrt 5 < 3 by SQUARE_1:def 2;
then (sqrt 5) - 1 < (2 + 1) - 1 by XREAL_1:9;
then - ((sqrt 5) - 1) > - 2 by XREAL_1:24;
then (1 - (sqrt 5)) / 2 > (- 2) / 2 by XREAL_1:74;
then A1: |.tau_bar.| < |.(- 1).| + |.0.| by FIB_NUM:def 2, MEASURE6:37;
|.(- 1).| = - (- 1) by ABSVALUE:def 1;
then |.tau_bar.| < 1 + 0 by A1;
hence |.tau_bar.| < 1 ; :: thesis: verum