theorem :: TMAP_1:37

for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )