theorem Th29: :: TOPS_2:29

for T being TopStruct
for M, N being Subset of T holds M /\ N is Subset of (T | N)