let K be SimplicialComplexStr; :: thesis: ( K is subset-closed implies TopStruct(# the carrier of K,the topology of K #) = Complex_of the topology of K )
assume K is subset-closed ; :: thesis: TopStruct(# the carrier of K,the topology of K #) = Complex_of the topology of K
then the_family_of K is subset-closed ;
hence TopStruct(# the carrier of K,the topology of K #) = Complex_of the topology of K by Th7; :: thesis: verum