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