2 < sqrt 5 by SQUARE_1:85, SQUARE_1:95;
then 1 < sqrt 5 by XXREAL_0:2;
then 1 + 1 < 1 + (sqrt 5) by XREAL_1:10;
then 2 / 2 < (1 + (sqrt 5)) / 2 by XREAL_1:76;
hence 1 < tau ; :: thesis: verum