let n be Nat; :: thesis: for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv,the topology of Kv #) = BCS n,Kv
let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds
TopStruct(# the carrier of Kv,the topology of Kv #) = BCS n,Kv
let Kv be non void SimplicialComplex of V; :: thesis: ( n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv,the topology of Kv #) = BCS n,Kv )
assume that
A1: n > 0 and
A2: |.Kv.| c= [#] Kv and
A3: degree Kv <= 0 ; :: thesis: TopStruct(# the carrier of Kv,the topology of Kv #) = BCS n,Kv
defpred S₁[ Nat] means ( $1 > 0 implies ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS $1,Kv & degree (BCS $1,Kv) <= 0 ) );
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

not {} in dom (center_of_mass V) by ZFMISC_1:64;
then A5: dom (center_of_mass V) is with_non-empty_elements by SETFAM_1:def 9;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
assume n + 1 > 0 ; :: thesis: ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS (n + 1),Kv & degree (BCS (n + 1),Kv) <= 0 )

per cases ( n = 0 or n > 0 ) ;

suppose A7: n = 0 ; :: thesis: ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS (n + 1),Kv & degree (BCS (n + 1),Kv) <= 0 )

A8: degree (subdivision (center_of_mass V),Kv) <= degree Kv by A5, SIMPLEX0:52;
BCS (n + 1),Kv = BCS Kv by A2, A7, Th17;
hence ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS (n + 1),Kv & degree (BCS (n + 1),Kv) <= 0 ) by A2, A3, A8, Def5, Th21; :: thesis: verum

end;

suppose A9: n > 0 ; :: thesis: ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS (n + 1),Kv & degree (BCS (n + 1),Kv) <= 0 )

A10: |.Kv.| = |.(BCS n,Kv).| by Th10;
[#] Kv = [#] (BCS n,Kv) by A6, A9;
then BCS n,Kv = BCS (BCS n,Kv) by A2, A6, A9, A10, Th21;
hence ( TopStruct(# the carrier of Kv,the topology of Kv #) = BCS (n + 1),Kv & degree (BCS (n + 1),Kv) <= 0 ) by A2, A6, A9, Th20; :: thesis: verum

end;

end;

end;

A11: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A4);
hence TopStruct(# the carrier of Kv,the topology of Kv #) = BCS n,Kv by A1; :: thesis: verum