tau - 1 = - tau_bar ;
then 0 + 1 < (tau - 1) + 1 by XREAL_1:6;
hence 1 < tau ; :: thesis: verum