theorem :: SIMPLEX0:39

for X being set
for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #)