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: abs tau_bar < (abs (- 1)) + (abs 0) by FIB_NUM:def 2, MEASURE6:37;
abs (- 1) = - (- 1) by ABSVALUE:def 1;
then abs tau_bar < 1 + 0 by A1;
hence abs tau_bar < 1 ; :: thesis: verum