let X be set ; :: thesis: for SC being SimplicialComplex of X
for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
let SC be SimplicialComplex of X; :: thesis: for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
let A, B be Subset of SC; :: thesis: ( A c= B implies SC | A is SubSimplicialComplex of SC | B )
A1: ( (bool A) /\ the topology of SC = the topology of (SC | A) & (bool B) /\ the topology of SC = the topology of (SC | B) ) by Th37;
assume A2: A c= B ; :: thesis: SC | A is SubSimplicialComplex of SC | B
then bool A c= bool B by ZFMISC_1:67;
then A3: (bool A) /\ the topology of SC c= (bool B) /\ the topology of SC by XBOOLE_1:27;
( [#] (SC | A) = A & [#] (SC | B) = B ) by Def16;
hence SC | A is SubSimplicialComplex of SC | B by A2, A3, A1, Def13; :: thesis: verum