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 12;
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