for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q in F holds
Q /\ M in F | M