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