for K being SimplicialComplexStr st K is subset-closed holds
TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K by Th7;