:: deftheorem Def7 defines space BORSUK_1:def 7 :
for X being TopSpace
for D being a_partition of the carrier of X
for b₃ being strict TopSpace holds
( b₃ = space D iff ( the carrier of b₃ = D & the topology of b₃ = { A where A is Subset of D : union A in the topology of X } ) );