:: deftheorem Def8 defines simplex-join-closed SIMPLEX1:def 8 :
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS holds
( Kr is simplex-join-closed iff for A, B being Subset of Kr st A is simplex-like & B is simplex-like holds
(conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) );