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