set E = the Element of D;
reconsider B = bool { the Element of D} as Subset-Family of D by 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 & T is total & not T is with_non-empty_elements & not T is empty-membered & T is finite-vertices & T is subset-closed & T is strict )
A1: Vertices T c= { the Element of D}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Vertices T or x in { the Element of D} )
assume A2: x in Vertices T ; :: thesis: x in { the Element of D}
reconsider v = x as Element of T by A2;
v is vertex-like by A2, Def4;
then consider S being Subset of T such that
A3: S is simplex-like and
A4: v in S by Def3;
S in B by A3, PRE_TOPC:def 2;
hence x in { the Element of D} by A4; :: thesis: verum

end;

{ the Element of D} in B by ZFMISC_1:def 1;
then not B is empty-membered by SETFAM_1:def 10;
then A5: ( [#] T = D & not T is empty-membered ) by Def7;
B = the_family_of T ;
then T is subset-closed by MATROID0:def 3;
hence ( not T is empty & T is total & not T is with_non-empty_elements & not T is empty-membered & T is finite-vertices & T is subset-closed & T is strict ) by A1, A5, Def5, Def10; :: thesis: verum