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

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