theorem :: SIMPLEX1:6

for x being set
for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V holds
( x in |.K.| iff ex A being Subset of K st
( A is simplex-like & x in Int (@ A) ) )