reconsider B = bool 0 as Subset-Family of D by XBOOLE_1:2, ZFMISC_1:67;
[#] TopStruct(# D,B #) c= D ;
then reconsider T = TopStruct(# D,B #) as SimplicialComplexStr of D by Def9;
take T ; :: thesis: ( not T is empty & not T is void & T is total & T is empty-membered & T is strict )
( [#] T = D & B is empty-membered ) ;
hence ( not T is empty & not T is void & T is total & T is empty-membered & T is strict ) by PENCIL_1:def 4; :: thesis: verum