:: deftheorem defines are_weakly_separated TSEP_1:def 7 :
for X being TopStruct
for X1, X2 being SubSpace of X holds
( X1,X2 are_weakly_separated iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated );