for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V
for SF being Subset-Family of K st SF = Sub_of_Fin the topology of K holds
Complex_of SF is SubdivisionStr of K