theorem :: TSEP_1:72

for X being non empty TopSpace
for X1, X2, Y being non empty SubSpace of X st X1 meets X2 & X1,Y are_separated holds
X1 meet X2,Y are_separated