let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let SX be SubSimplicialComplex of KX; :: thesis: for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
let S1 be SubSimplicialComplex of SX; :: thesis: ( SX is maximal & S1 is maximal implies S1 is maximal SubSimplicialComplex of KX )
reconsider s1 = S1 as SubSimplicialComplex of KX by Th27;
assume that
A1: SX is maximal and
A2: S1 is maximal ; :: thesis: S1 is maximal SubSimplicialComplex of KX
A3: [#] S1 c= [#] SX by Def13;

now :: thesis: for A being Subset of s1 st A in the topology of KX holds
A is simplex-like

let A be Subset of s1; :: thesis: ( A in the topology of KX implies A is simplex-like )
reconsider a = A as Subset of SX by A3, XBOOLE_1:1;
assume A in the topology of KX ; :: thesis: A is simplex-like
then a is simplex-like by A1;
then a in the topology of SX ;
hence A is simplex-like by A2; :: thesis: verum

end;

hence S1 is maximal SubSimplicialComplex of KX by Def14; :: thesis: verum