the_family_of KX is subset-closed ;
then reconsider BA = (bool A) /\ the topology of KX as finite-membered subset-closed Subset-Family of A by A1, XBOOLE_1:17;
set KA = TopStruct(# A,BA #);
A2: ( [#] TopStruct(# A,BA #) c= [#] KX & the topology of TopStruct(# A,BA #) c= the topology of KX ) by XBOOLE_1:17;
A3: ( TopStruct(# A,BA #) is subset-closed & TopStruct(# A,BA #) is finite-membered ) ;
[#] KX c= X by Def9;
then [#] TopStruct(# A,BA #) c= X ;
then TopStruct(# A,BA #) is SimplicialComplexStr of X by Def9;
then reconsider KA = TopStruct(# A,BA #) as strict maximal SubSimplicialComplex of KX by A2, A3, Def13, Th33;
take KA ; :: thesis: [#] KA = A
thus [#] KA = A ; :: thesis: verum