theorem :: TSEP_1:66

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 union X2 is closed SubSpace of X & X1,X2 are_separated holds
X1 is closed SubSpace of X