theorem Th5: :: SIMPLEX1:5
for RLS being non empty RLSStruct
for Kr being SimplicialComplexStr of RLS
for A being Subset of Kr st A is simplex-like holds
conv (@ A) c= |.Kr.| by Def3;