sqrt 5 < sqrt (3 ^2 ) by SQUARE_1:95;
then sqrt 5 < 3 by SQUARE_1:def 4;
then (sqrt 5) - 1 < (2 + 1) - 1 by XREAL_1:11;
then - ((sqrt 5) - 1) > - 2 by XREAL_1:26;
then (1 - (sqrt 5)) / 2 > (- 2) / 2 by XREAL_1:76;
then A1: abs tau_bar < (abs (- 1)) + (abs 0 ) by FIB_NUM:def 2, MEASURE6:73;
abs (- 1) = - (- 1) by ABSVALUE:def 1;
then abs tau_bar < 1 + 0 by A1;
hence abs tau_bar < 1 ; :: thesis: verum