:: deftheorem defines Complex_of SIMPLEX0:def 11 :
for X being set
for Y being Subset-Family of X holds Complex_of Y = TopStruct(# X,(subset-closed_closure_of Y) #);