set T = TopStruct(# 0,({} (bool 0)) #);
( the_family_of TopStruct(# 0,({} (bool 0)) #) is empty & [#] TopStruct(# 0,({} (bool 0)) #) c= X ) ;
then reconsider T = TopStruct(# 0,({} (bool 0)) #) as SimplicialComplex of X by Def9, MATROID0:def 3, MATROID0:def 6;
take T ; :: thesis: ( [#] T c= [#] KX & the topology of T c= the topology of KX )
thus ( [#] T c= [#] KX & the topology of T c= the topology of KX ) ; :: thesis: verum