let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision P,KX) st dom P c= the topology of SX & A = [#] SX holds
subdivision P,SX = (subdivision P,KX) | A
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision P,KX) st dom P c= the topology of SX & A = [#] SX holds
subdivision P,SX = (subdivision P,KX) | A
let SX be SubSimplicialComplex of KX; :: thesis: for P being Function
for A being Subset of (subdivision P,KX) st dom P c= the topology of SX & A = [#] SX holds
subdivision P,SX = (subdivision P,KX) | A
let P be Function; :: thesis: for A being Subset of (subdivision P,KX) st dom P c= the topology of SX & A = [#] SX holds
subdivision P,SX = (subdivision P,KX) | A
set PK = subdivision P,KX;
reconsider PS = subdivision P,SX as strict SubSimplicialComplex of subdivision P,KX by Th58;
let A be Subset of (subdivision P,KX); :: thesis: ( dom P c= the topology of SX & A = [#] SX implies subdivision P,SX = (subdivision P,KX) | A )
assume that
A1: dom P c= the topology of SX and
A2: A = [#] SX ; :: thesis: subdivision P,SX = (subdivision P,KX) | A

now

let a be Subset of PS; :: thesis: ( a in the topology of (subdivision P,KX) implies a is simplex-like )
assume a in the topology of (subdivision P,KX) ; :: thesis: a is simplex-like
then reconsider b = a as Simplex of (subdivision P,KX) by PRE_TOPC:def 5;
consider SS being c=-linear finite simplex-like Subset-Family of KX such that
A3: b = P .: SS by Def20;
SS /\ (dom P) c= dom P by XBOOLE_1:17;
then A4: SS /\ (dom P) c= the topology of SX by A1, XBOOLE_1:1;
SS /\ (dom P) c= SS by XBOOLE_1:17;
then reconsider Sd = SS /\ (dom P) as c=-linear finite Subset-Family of SX by A4, XBOOLE_1:1;
A5: Sd is simplex-like

proof

let B be Subset of SX; :: according to TOPS_2:def 1 :: thesis: ( not B in Sd or B is simplex-like )
assume B in Sd ; :: thesis: B is simplex-like
then B in dom P by XBOOLE_0:def 4;
hence B is simplex-like by A1, PRE_TOPC:def 5; :: thesis: verum

end;

P .: SS = P .: Sd by RELAT_1:145;
hence a is simplex-like by A3, A5, Def20; :: thesis: verum

end;

then A6: PS is maximal by Def14;
[#] PS = [#] SX by Def20;
hence subdivision P,SX = (subdivision P,KX) | A by A2, A6, Def16; :: thesis: verum