let X be set ; :: thesis: for SC being SimplicialComplex of X
for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let SC be SimplicialComplex of X; :: thesis: for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let A, B be Subset of SC; :: thesis: for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
let B1 be Subset of (SC | A); :: thesis: ( B1 = B implies (SC | A) | B1 = SC | B )
reconsider SCAB = (SC | A) | B1 as strict maximal SubSimplicialComplex of SC by Th34;
assume A1: B1 = B ; :: thesis: (SC | A) | B1 = SC | B
[#] SCAB = B1 by Def16;
hence (SC | A) | B1 = SC | B by A1, Def16; :: thesis: verum