A1: ( - 1 <= t & t <= 1 & - 1 <= u & u <= 1 ) by Def1;
then A2: ( (- 1) * (- 1) >= (- 1) * u & (- 1) * u >= (- 1) * 1 ) by XREAL_1:65;

per cases ( 0 <= u or u < 0 ) ;

suppose 0 <= u ; :: thesis: t * u is theta

then ( (- 1) * u <= t * u & t * u <= 1 * u ) by A1, XREAL_1:64;
hence t * u is theta by A1, A2, XXREAL_0:2; :: thesis: verum

end;

suppose u < 0 ; :: thesis: t * u is theta

then ( (- 1) * u >= t * u & t * u >= 1 * u ) by A1, XREAL_1:65;
hence t * u is theta by A1, A2, XXREAL_0:2; :: thesis: verum

end;

end;