( 0 <= s & 0 <= t & s <= 1 & t <= 1 ) by BORSUK_1:43;
hence s * t is Point of I[01] by BORSUK_1:43, XREAL_1:160; :: thesis: verum