theorem Th28: :: TMAP_1:28

for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & ( X0 misses X2 or X2 misses X0 ) holds
( X0 meet (X1 union X2) = TopStruct(# the carrier of X1, the topology of X1 #) & X0 meet (X2 union X1) = TopStruct(# the carrier of X1, the topology of X1 #) )