let X be set ; :: thesis: for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1
let A be finite Subset of X; :: thesis: degree (Complex_of {A}) = (card A) - 1
set C = Complex_of {A};
A1: the topology of (Complex_of {A}) = bool A by Th4;

now

let S be finite Subset of (Complex_of {A}); :: thesis: ( S is simplex-like implies card S <= ((card A) - 1) + 1 )
assume S is simplex-like ; :: thesis: card S <= ((card A) - 1) + 1
then S in the topology of (Complex_of {A}) by PRE_TOPC:def 5;
hence card S <= ((card A) - 1) + 1 by A1, NAT_1:44; :: thesis: verum

end;

then A2: degree (Complex_of {A}) <= (card A) - 1 by Th25;
A c= A ;
then reconsider A1 = A as finite Simplex of (Complex_of {A}) by A1, PRE_TOPC:def 5;
( card A = ((card A) - 1) + 1 & card A1 <= (degree (Complex_of {A})) + 1 ) by Def12;
then (card A) - 1 <= degree (Complex_of {A}) by XREAL_1:10;
hence (card A) - 1 = degree (Complex_of {A}) by A2, XXREAL_0:1; :: thesis: verum