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