|.tau_bar.| = - tau_bar by ABSVALUE:def 1;
then (- tau_bar) - 1 < 0 by XREAL_1:49, FIB_NUM4:5;
then (tau - 2) + 2 < 0 + 2 by XREAL_1:6;
hence tau < 2 ; :: thesis: verum