theorem :: SIMPLEX1:27

for V being RealLinearSpace
for Ks being simplex-join-closed SimplicialComplex of V
for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds
( Int (@ As) c= conv (@ Bs) iff As c= Bs )