the carrier of I(01) = ].0,1.[ by Def1;
hence not the carrier of I(01) is empty by XXREAL_1:33; :: according to STRUCT_0:def 1 :: thesis: verum