:: deftheorem Def2 defines [: BORSUK_1:def 2 :
for X, Y being TopSpace
for b₃ being strict TopSpace holds
( b₃ = [:X,Y:] iff ( the carrier of b₃ = [: the carrier of X, the carrier of Y:] & the topology of b₃ = { (union A) where A is Subset-Family of b₃ : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ) );