defpred S₁[ Nat] means subdivision $1,(center_of_mass V),Kv is non void Subdivision of Kv;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider P = subdivision k,(center_of_mass V),Kv as non void Subdivision of Kv ;
A3: ( |.P.| = |.Kv.| & [#] P = [#] Kv ) by Th10, SIMPLEX0:64;
k in NAT by ORDINAL1:def 13;
then subdivision (k + 1),(center_of_mass V),Kv = subdivision 1,(center_of_mass V),(subdivision k,(center_of_mass V),Kv) by SIMPLEX0:63
.= subdivision (center_of_mass V),P by SIMPLEX0:62
.= BCS P by A1, A3, Def5 ;
hence S₁[k + 1] by Th14; :: thesis: verum

end;

Kv = subdivision 0 ,(center_of_mass V),Kv by SIMPLEX0:61;
then A4: S₁[ 0 ] by Th11;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence subdivision n,(center_of_mass V),Kv is non void Subdivision of Kv ; :: thesis: verum