set C = Complex_of ({} (bool {}));
the topology of (Complex_of ({} (bool {}))) = {} ;
then A1: ( [#] (Complex_of ({} (bool {}))) c= [#] KX & the topology of (Complex_of ({} (bool {}))) c= the topology of KX ) by XBOOLE_1:2;
[#] (Complex_of ({} (bool {}))) c= X by XBOOLE_1:2;
then Complex_of ({} (bool {})) is SimplicialComplexStr of X by Def9;
then reconsider C = Complex_of ({} (bool {})) as SubSimplicialComplex of KX by A1, Def13;
take C ; :: thesis: ( C is empty & C is void & C is strict )
thus ( C is empty & C is void & C is strict ) ; :: thesis: verum