reconsider E = ].0,1.[ as non empty Subset of I[01] by BORSUK_1:83, XXREAL_1:25, XXREAL_1:33;
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:29; :: thesis: verum