let X be 1-sorted ; :: thesis: for K being subset-closed SimplicialComplexStr of X st K is total holds
for S being finite Subset of K st not S is dependent holds
Complex_of {(@ S)} is SubSimplicialComplex of K
let K be subset-closed SimplicialComplexStr of X; :: thesis: ( K is total implies for S being finite Subset of K st not S is dependent holds
Complex_of {(@ S)} is SubSimplicialComplex of K )
assume A1: K is total ; :: thesis: for S being finite Subset of K st not S is dependent holds
Complex_of {(@ S)} is SubSimplicialComplex of K
let S be finite Subset of K; :: thesis: ( not S is dependent implies Complex_of {(@ S)} is SubSimplicialComplex of K )
assume A2: not S is dependent ; :: thesis: Complex_of {(@ S)} is SubSimplicialComplex of K
S in the topology of K by A2, PRE_TOPC:def 2;
then A3: {S} c= the topology of K by ZFMISC_1:31;
set C = Complex_of {(@ S)};
A4: [#] (Complex_of {(@ S)}) c= [#] K by A1, SIMPLEX0:def 10;
the_family_of K is subset-closed ;
then the topology of (Complex_of {(@ S)}) c= the topology of K by A3, SIMPLEX0:def 1;
hence Complex_of {(@ S)} is SubSimplicialComplex of K by A4, SIMPLEX0:def 13; :: thesis: verum