theorem Th29: :: TMAP_1:29

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