for X being set
for SC being SimplicialComplex of X
for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B