for X being set
for Y1, Y2 being Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds
Complex_of Y1 is SubSimplicialComplex of Complex_of Y2