let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for A being Subset of KX
for S being finite-membered Subset-Family of A st subset-closed_closure_of S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let KX be SimplicialComplexStr of X; :: thesis: for A being Subset of KX
for S being finite-membered Subset-Family of A st subset-closed_closure_of S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let A be Subset of KX; :: thesis: for S being finite-membered Subset-Family of A st subset-closed_closure_of S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let S be finite-membered Subset-Family of A; :: thesis: ( subset-closed_closure_of S c= the topology of KX implies Complex_of S is strict SubSimplicialComplex of KX )
assume A1: subset-closed_closure_of S c= the topology of KX ; :: thesis: Complex_of S is strict SubSimplicialComplex of KX
set C = Complex_of S;
[#] KX c= X by Def9;
then [#] (Complex_of S) c= X ;
then ( [#] (Complex_of S) c= [#] KX & Complex_of S is strict SimplicialComplexStr of X ) by Def9;
hence Complex_of S is strict SubSimplicialComplex of KX by A1, Def13; :: thesis: verum