:: deftheorem Def1 defines I(01) BORSUK_4:def 1 :
for b₁ being strict SubSpace of I[01] holds
( b₁ = I(01) iff the carrier of b₁ = ].0,1.[ );