let S be SubSimplicialComplex of KX; :: thesis: S is void
( the topology of S c= the topology of KX & the topology of KX is empty ) by Def13, PENCIL_1:def 4;
hence S is void ; :: thesis: verum