let x be set ; :: thesis: for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
let K be SimplicialComplexStr; :: thesis: for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K
let S be Subset of K; :: thesis: ( S is simplex-like & x in S implies x in Vertices K )
assume that
A1: S is simplex-like and
A2: x in S ; :: thesis: x in Vertices K
reconsider v = x as Element of K by A2;
v is vertex-like by A1, A2;
hence x in Vertices K by Def4; :: thesis: verum