set B = { v where v is Element of K : v is vertex-like } ;
{ v where v is Element of K : v is vertex-like } c= [#] K

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of K : v is vertex-like } or x in [#] K )
assume x in { v where v is Element of K : v is vertex-like } ; :: thesis: x in [#] K
then consider v being Element of K such that
A1: x = v and
A2: v is vertex-like ;
ex S being Subset of K st
( S is simplex-like & v in S ) by A2;
hence x in [#] K by A1; :: thesis: verum

end;

then reconsider B = { v where v is Element of K : v is vertex-like } as Subset of K ;
take B ; :: thesis: for v being Element of K holds
( v in B iff v is vertex-like )
let v be Element of K; :: thesis: ( v in B iff v is vertex-like )

hereby :: thesis: ( v is vertex-like implies v in B )

assume v in B ; :: thesis: v is vertex-like
then ex w being Element of K st
( v = w & w is vertex-like ) ;
hence v is vertex-like ; :: thesis: verum

end;

assume v is vertex-like ; :: thesis: v in B
hence v in B ; :: thesis: verum