:: deftheorem Def2 defines union TSEP_1:def 2 :
for X being non empty TopStruct
for X1, X2 being non empty SubSpace of X
for b₄ being non empty strict SubSpace of X holds
( b₄ = X1 union X2 iff the carrier of b₄ = the carrier of X1 \/ the carrier of X2 );