set C = Complex_of ({} (bool {}));
A1: ( [#] (Complex_of ({} (bool {}))) c= [#] KX & the topology of (Complex_of ({} (bool {}))) c= the topology of KX ) ;
[#] (Complex_of ({} (bool {}))) c= X ;
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