let X be set ; :: thesis: for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX
for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
let KX be subset-closed SimplicialComplexStr of X; :: thesis: for A being Subset of KX
for S being finite-membered Subset-Family of A st 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 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: ( S c= the topology of KX implies Complex_of S is strict SubSimplicialComplex of KX )
A1: the_family_of KX is subset-closed ;
assume S c= the topology of KX ; :: thesis: Complex_of S is strict SubSimplicialComplex of KX
hence Complex_of S is strict SubSimplicialComplex of KX by A1, Th3, Th28; :: thesis: verum