:: deftheorem defines I[01]-TIMES TOPALG_7:def 6 :
I[01]-TIMES = R^1-TIMES || (R^1 [.0,1.]);