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 S1[ 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 S1[n] holds
S1[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: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[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: S1[ 0 ] ;
for n being Nat holds S1[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