theorem Th25: :: SIMPLEX1:25

for V being RealLinearSpace
for K being subset-closed SimplicialComplexStr of V holds
( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B )