( 1 > 0 & sqrt 5 > 0 ) by SQUARE_1:93;
then 1 + (sqrt 5) > 0 + 0 ;
hence tau > 0 by FIB_NUM:def 1, XREAL_1:141; :: thesis: verum