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