:: deftheorem Def3 defines |. SIMPLEX1:def 3 :
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for b₃ being Subset of RLS holds
( b₃ = |.Kr.| iff for x being set holds
( x in b₃ iff ex A being Subset of Kr st
( A is simplex-like & x in conv (@ A) ) ) );