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