:: deftheorem defines simplicial CHORD:def 7 :
for G being _Graph
for v being Vertex of G holds
( v is simplicial iff ( G .AdjacentSet {v} <> {} implies for G2 being AdjGraph of G,{v} holds G2 is complete ) );