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 )
proof
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;
assume |.Ka.| c= [#] Ka ; :: thesis: degree Ka = degree (BCS Ka)
hence degree Ka = degree (BCS Ka) by A1, Th30; :: thesis: verum