[#] TopStruct(# {},({} (bool {})) #) c= X ;
then reconsider T = TopStruct(# {},({} (bool {})) #) as SimplicialComplexStr of X by Def9;
take T ; :: thesis: ( T is empty & T is void & T is empty-membered & T is strict )
thus ( T is empty & T is void & T is empty-membered & T is strict ) ; :: thesis: verum