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 )
for x being non empty set holds not x in B ;
then ( [#] T = D & B is empty-membered ) by SETFAM_1:def 10;
hence ( not T is empty & not T is void & T is total & T is empty-membered & T is strict ) by Def7, Def10, PENCIL_1:def 4; :: thesis: verum