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:56;
then A5: dom (center_of_mass V) is with_non-empty_elements ;
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