let K be non void subset-closed SimplicialComplexStr; :: thesis: for S being finite Simplex of K holds S is Simplex of (card S) - 1,K
let S be finite Simplex of K; :: thesis: S is Simplex of (card S) - 1,K
card S <= (degree K) + 1 by Th24;
then (card S) - 1 <= ((degree K) + 1) - 1 by XXREAL_3:37;
then A1: (card S) - 1 <= degree K by XXREAL_3:24;
( (card S) - 1 >= 0 - 1 & card S = ((card S) - 1) + 1 ) by XREAL_1:6;
hence S is Simplex of (card S) - 1,K by A1, Def18; :: thesis: verum