( - 1 <= t & t <= 1 ) by Def1;
then ( (- 1) * (- 1) >= (- 1) * t & (- 1) * t >= (- 1) * 1 ) by XREAL_1:65;
hence - t is theta ; :: thesis: verum