theorem :: TOPS_2:32

for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)