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