:: deftheorem Def19 defines Face SIMPLEX0:def 19 :
for K being non void subset-closed SimplicialComplexStr
for i being Real st i is integer & i <= degree K holds
for S being Simplex of i,K
for b₄ being Simplex of max ((i - 1),(- 1)),K holds
( b₄ is Face of S iff b₄ c= S );