let X be set ; :: thesis: for SC being SimplicialComplex of X
for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
let SC be SimplicialComplex of X; :: thesis: for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
let A be Subset of SC; :: thesis: the topology of (SC | A) = (bool A) /\ the topology of SC
A1: [#] (SC | A) = A by Def16;
then A2: (bool A) /\ the topology of SC c= the topology of (SC | A) by Th33;
the topology of (SC | A) c= the topology of SC by Def13;
then the topology of (SC | A) c= (bool A) /\ the topology of SC by A1, XBOOLE_1:19;
hence the topology of (SC | A) = (bool A) /\ the topology of SC by A2; :: thesis: verum