sqrt 5 > 0 by SQUARE_1:93;
hence tau > 0 by FIB_NUM:def 1, XREAL_1:141; :: thesis: verum