:: deftheorem defines constitute_a_decomposition TSEP_2:def 2 :
for X being non empty TopSpace
for X1, X2 being SubSpace of X holds
( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition );