for G being _Graph
for v being Vertex of G st v is simplicial holds
for a, b being object st a <> b & a in G .AdjacentSet {v} & b in G .AdjacentSet {v} holds
ex e being object st e Joins a,b,G