reconsider E = ].0,1.[ as Subset of I[01] by BORSUK_1:40, XXREAL_1:25;
take I[01] | E ; :: thesis: the carrier of (I[01] | E) = ].0,1.[
thus the carrier of (I[01] | E) = ].0,1.[ by PRE_TOPC:8; :: thesis: verum