let X be set ; :: thesis: for n being Nat
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX
let n be Nat; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for P being Function holds subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX
let SX be SubSimplicialComplex of KX; :: thesis: for P being Function holds subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX
let P be Function; :: thesis: subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX
defpred S₁[ Nat] means subdivision $1,P,SX is SubSimplicialComplex of subdivision $1,P,KX;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider Pn = subdivision n,P,SX as SubSimplicialComplex of subdivision n,P,KX ;
A2: n in NAT by ORDINAL1:def 13;
then A3: subdivision (n + 1),P,SX = subdivision 1,P,Pn by Th63
.= subdivision P,Pn by Th62 ;
subdivision (n + 1),P,KX = subdivision 1,P,(subdivision n,P,KX) by A2, Th63
.= subdivision P,(subdivision n,P,KX) by Th62 ;
hence S₁[n + 1] by A3, Th58; :: thesis: verum

end;

subdivision 0 ,P,SX = SX by Th61;
then A4: S₁[ 0 ] by Th61;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence subdivision n,P,SX is SubSimplicialComplex of subdivision n,P,KX ; :: thesis: verum