A1: the carrier of I(01) = ].0 ,1.[ by Def1;
[.0 ,1.] = ].0 ,1.[ \/ {0 ,1} by XXREAL_1:128;
hence the carrier of I(01) = the carrier of I[01] \ {0 ,1} by A1, BORSUK_1:83, XBOOLE_1:88, XXREAL_1:86; :: thesis: verum