reconsider f = I[01]-TIMES as Function of [:I[01],I[01]:],R^1 by TOPREALA:7;

f is continuous by Th5, TOPMETR:7;

hence I[01]-TIMES is continuous by PRE_TOPC:27; :: thesis: verum

f is continuous by Th5, TOPMETR:7;

hence I[01]-TIMES is continuous by PRE_TOPC:27; :: thesis: verum