defpred S_{1}[ Nat] means subdivision ($1,(center_of_mass V),Kv) is non void Subdivision of Kv;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A4: S_{1}[ 0 ]
by Th11;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A4, A2);

hence subdivision (n,(center_of_mass V),Kv) is non void Subdivision of Kv ; :: thesis: verum

A2: for k being Nat st S

S

proof

Kv = subdivision (0,(center_of_mass V),Kv)
by SIMPLEX0:61;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by Th14; :: thesis: verum

end;assume S

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

then A4: S

for k being Nat holds S

hence subdivision (n,(center_of_mass V),Kv) is non void Subdivision of Kv ; :: thesis: verum