let K be SimplicialComplexStr; :: thesis: for A being Subset of K st A is simplex-like holds
A c= Vertices K
let A be Subset of K; :: thesis: ( A is simplex-like implies A c= Vertices K )
assume A1: A is simplex-like ; :: thesis: A c= Vertices K
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Vertices K )
thus ( not x in A or x in Vertices K ) by A1, Lm3; :: thesis: verum