let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let SX be SubSimplicialComplex of KX; :: thesis: for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
let S1 be SubSimplicialComplex of SX; :: thesis: S1 is SubSimplicialComplex of KX
( [#] SX c= [#] KX & [#] S1 c= [#] SX ) by Def13;
then A1: [#] S1 c= [#] KX ;
( the topology of SX c= the topology of KX & the topology of S1 c= the topology of SX ) by Def13;
then the topology of S1 c= the topology of KX ;
hence S1 is SubSimplicialComplex of KX by A1, Def13; :: thesis: verum