let p, q be Point of I[01]; :: thesis: p * q is Point of I[01]
A1: 0 <= p by BORSUK_1:43;
( p <= 1 & q <= 1 ) by BORSUK_1:43;
then ( 0 <= q & p * q <= 1 ) by A1, BORSUK_1:43, XREAL_1:160;
hence p * q is Point of I[01] by A1, BORSUK_1:43; :: thesis: verum