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 & T is with_empty_element & T is with_non-empty_element & T is finite-vertices & T is subset-closed & T is strict )
A1: Vertices T c= { the Element of D}

proof

let x be object ; :: 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 ;
S in B by A3;
hence x in { the Element of D} by A4; :: thesis: verum

end;

{ the Element of D} in B by ZFMISC_1:def 1;
then B is with_non-empty_element ;
then A5: ( [#] T = D & T is with_non-empty_element ) ;
thus ( not T is empty & T is total & T is with_empty_element & T is with_non-empty_element & T is finite-vertices & T is subset-closed & T is strict ) by A1, A5; :: thesis: verum