let V be RealLinearSpace; :: thesis: for Ka being non void affinely-independent SimplicialComplex of V st |.Ka.| c= [#] Ka holds

degree Ka = degree (BCS Ka)

let Ka be non void affinely-independent SimplicialComplex of V; :: thesis: ( |.Ka.| c= [#] Ka implies degree Ka = degree (BCS Ka) )

A1: for n being Nat st n <= degree Ka holds

ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent )

hence degree Ka = degree (BCS Ka) by A1, Th30; :: thesis: verum

degree Ka = degree (BCS Ka)

let Ka be non void affinely-independent SimplicialComplex of V; :: thesis: ( |.Ka.| c= [#] Ka implies degree Ka = degree (BCS Ka) )

A1: for n being Nat st n <= degree Ka holds

ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent )

proof

assume
|.Ka.| c= [#] Ka
; :: thesis: degree Ka = degree (BCS Ka)
let n be Nat; :: thesis: ( n <= degree Ka implies ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent ) )

reconsider N = n as ExtReal ;

set S = the Simplex of n,Ka;

assume n <= degree Ka ; :: thesis: ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent )

then A2: card the Simplex of n,Ka = N + 1 by SIMPLEX0:def 18;

( N + 1 = n + 1 & @ the Simplex of n,Ka is affinely-independent ) by XXREAL_3:def 2;

hence ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent ) by A2; :: thesis: verum

end;( card S = n + 1 & @ S is affinely-independent ) )

reconsider N = n as ExtReal ;

set S = the Simplex of n,Ka;

assume n <= degree Ka ; :: thesis: ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent )

then A2: card the Simplex of n,Ka = N + 1 by SIMPLEX0:def 18;

( N + 1 = n + 1 & @ the Simplex of n,Ka is affinely-independent ) by XXREAL_3:def 2;

hence ex S being Simplex of Ka st

( card S = n + 1 & @ S is affinely-independent ) by A2; :: thesis: verum

hence degree Ka = degree (BCS Ka) by A1, Th30; :: thesis: verum