let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let SX be SubSimplicialComplex of KX; :: thesis: for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
let S1 be SubSimplicialComplex of SX; :: thesis: ( S1 is maximal SubSimplicialComplex of KX implies S1 is maximal )
assume S1 is maximal SubSimplicialComplex of KX ; :: thesis: S1 is maximal
then reconsider s1 = S1 as maximal SubSimplicialComplex of KX ;
the topology of SX c= the topology of KX by Def13;
then A1: (bool ([#] s1)) /\ the topology of SX c= (bool ([#] s1)) /\ the topology of KX by XBOOLE_1:26;
(bool ([#] s1)) /\ the topology of KX c= the topology of s1 by Th33;
then (bool ([#] S1)) /\ the topology of SX c= the topology of S1 by A1;
hence S1 is maximal by Th33; :: thesis: verum