for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like holds
S c= Vertices K by Lm4;