[#] TopStruct(# X,(subset-closed_closure_of Y) #) = X ;
hence TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X by Def9; :: thesis: verum