let X be set ; for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1
let A be finite Subset of X; degree (Complex_of {A}) = (card A) - 1
set C = Complex_of {A};
A1:
the topology of (Complex_of {A}) = bool A
by Th4;
then
for S being finite Subset of (Complex_of {A}) st S is simplex-like holds
card S <= ((card A) - 1) + 1
by NAT_1:43;
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 2;
( 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:8;
hence
(card A) - 1 = degree (Complex_of {A})
by A2, XXREAL_0:1; verum