:: deftheorem defines .AdjacentSet CHORD:def 4 :
for G being _Graph
for S being set holds G .AdjacentSet S = { u where u is Vertex of G : ( not u in S & ex v being Vertex of G st
( v in S & u,v are_adjacent ) ) } ;