:: deftheorem Def13 defines I[01] BORSUK_1:def 13 :
for b₁ being TopStruct holds
( b₁ = I[01] iff for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds
b₁ = (TopSpaceMetr RealSpace) | P );