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 S is simplex-like 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 S is simplex-like holds
Complex_of {(@ S)} is SubSimplicialComplex of K )
assume A1: K is total ; :: thesis: for S being finite Subset of K st S is simplex-like holds
Complex_of {(@ S)} is SubSimplicialComplex of K
let S be finite Subset of K; :: thesis: ( S is simplex-like implies Complex_of {(@ S)} is SubSimplicialComplex of K )
assume A2: S is simplex-like ; :: thesis: Complex_of {(@ S)} is SubSimplicialComplex of K
S in the topology of K by A2;
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;
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