2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27;
then not 0 + (sqrt 5) <= 1 by XXREAL_0:2;
then 0 * 2 > (1 - (sqrt 5)) / 1 by XREAL_1:19;
then (1 - (sqrt 5)) / 2 < 0 * 1 by XREAL_1:113;
hence tau_bar < 0 ; :: thesis: verum