let X be set ; :: thesis: for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC,the topology of SC #)
let SC be SimplicialComplex of X; :: thesis: SC | ([#] SC) = TopStruct(# the carrier of SC,the topology of SC #)
set T = TopStruct(# the carrier of SC,the topology of SC #);
A1: ( [#] TopStruct(# the carrier of SC,the topology of SC #) c= [#] SC & (bool ([#] TopStruct(# the carrier of SC,the topology of SC #))) /\ the topology of SC = the topology of SC ) by XBOOLE_1:28;
( the_family_of SC = the_family_of TopStruct(# the carrier of SC,the topology of SC #) & the_family_of SC is finite-membered & the_family_of SC is subset-closed ) by MATROID0:def 6;
then A2: ( TopStruct(# the carrier of SC,the topology of SC #) is finite-membered & TopStruct(# the carrier of SC,the topology of SC #) is subset-closed ) by MATROID0:def 3, MATROID0:def 6;
[#] SC c= X by Def9;
then [#] TopStruct(# the carrier of SC,the topology of SC #) c= X ;
then TopStruct(# the carrier of SC,the topology of SC #) is SimplicialComplexStr of X by Def9;
then reconsider T = TopStruct(# the carrier of SC,the topology of SC #) as maximal SubSimplicialComplex of SC by A1, A2, Def13, Th33;
[#] T = [#] SC ;
hence SC | ([#] SC) = TopStruct(# the carrier of SC,the topology of SC #) by Def16; :: thesis: verum