let KA be strict maximal SubSimplicialComplex of SC; :: thesis: ( KA = SC | A iff [#] KA = A )
( the_family_of SC is finite-membered & (bool A) /\ the topology of SC c= the topology of SC ) by MATROID0:def 6, XBOOLE_1:17;
hence ( KA = SC | A iff [#] KA = A ) by Def15; :: thesis: verum