set B = (bool {}) /\ the topology of KX;
reconsider B = (bool {}) /\ the topology of KX as finite-membered subset-closed Subset-Family of ({} KX) by XBOOLE_1:17, ZFMISC_1:1, ZFMISC_1:33;
subset-closed_closure_of B = B by Th7;
then reconsider C = Complex_of B as strict SubSimplicialComplex of KX by Th28, XBOOLE_1:17;
take C ; :: thesis: ( C is maximal & C is strict )
( C = TopStruct(# ({} KX),B #) & bool ([#] C) = bool {} ) by Th7;
hence ( C is maximal & C is strict ) by Th33; :: thesis: verum