2 < sqrt 5 by SQUARE_1:20, SQUARE_1:27;
then 1 < sqrt 5 by XXREAL_0:2;
then 1 + 1 < 1 + (sqrt 5) by XREAL_1:8;
then 2 / 2 < (1 + (sqrt 5)) / 2 by XREAL_1:74;
hence 1 < tau ; :: thesis: verum