let a, b be Element of [.0,1.]; :: thesis: a * b in [.0,1.]
A0: ( 1 >= a & a >= 0 & 1 >= b & b >= 0 ) by XXREAL_1:1;
then 1 >= a * b by XREAL_1:160;
hence a * b in [.0,1.] by XXREAL_1:1, A0; :: thesis: verum