the_family_of KX is subset-closed ;
then reconsider BA = (bool A) /\ the topology of KX as subset-closed finite-membered 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;
BA = the_family_of TopStruct(# A,BA #) ;
then A3: ( TopStruct(# A,BA #) is subset-closed & TopStruct(# A,BA #) is finite-membered ) by MATROID0:def 3, MATROID0:def 6;
[#] KX c= X by Def9;
then [#] TopStruct(# A,BA #) c= X by XBOOLE_1:1;
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