A1: the_family_of KD is subset-closed ;
consider x being object such that
A2: x in the topology of KD by XBOOLE_0:def 1;
reconsider x = x as set by TARSKI:1;

per cases ( x is empty or not x is empty ) ;

suppose x is empty ; :: thesis: not for b₁ being SubSimplicialComplex of KD holds b₁ is void

then reconsider x = x as empty Subset of KD by A2;
set S = Complex_of {x};
A3: [#] (Complex_of {x}) = [#] KD ;
[#] KD c= D by Def9;
then reconsider S = Complex_of {x} as SimplicialComplex of D by A3, Def9;
take S ; :: thesis: ( S is SubSimplicialComplex of KD & not S is void )
{x} c= the topology of KD by A2, ZFMISC_1:31;
then subset-closed_closure_of {x} c= the topology of KD by A1, Th3;
hence ( S is SubSimplicialComplex of KD & not S is void ) by A3, Def13; :: thesis: verum

end;

suppose A4: not x is empty ; :: thesis: not for b₁ being SubSimplicialComplex of KD holds b₁ is void

set d = the Element of x;
the Element of x in x by A4;
then reconsider dd = { the Element of x} as Subset of KD by A2, ZFMISC_1:31;
set S = Complex_of {dd};
A5: [#] (Complex_of {dd}) = [#] KD ;
[#] KD c= D by Def9;
then reconsider S = Complex_of {dd} as SimplicialComplex of D by A5, Def9;
take S ; :: thesis: ( S is SubSimplicialComplex of KD & not S is void )
dd c= x by A4, ZFMISC_1:31;
then dd in the topology of KD by A1, A2;
then {dd} c= the topology of KD by ZFMISC_1:31;
then the topology of S c= the topology of KD by A1, Th3;
hence ( S is SubSimplicialComplex of KD & not S is void ) by A5, Def13; :: thesis: verum

end;

end;