theorem :: SIMPLEX0:26

for X being set
for A being finite Subset of X holds degree (Complex_of {A}) = (card A) - 1