set T = TopStruct(# 0 ,({} (bool 0 )) #);
( the_family_of TopStruct(# 0 ,({} (bool 0 )) #) is empty & [#] TopStruct(# 0 ,({} (bool 0 )) #) c= X ) by XBOOLE_1:2;
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 ) by XBOOLE_1:2; :: thesis: verum