:: deftheorem Def5 defines AdjGraph CHORD:def 5 :
for G being _Graph
for S being set
for b₃ being Subgraph of G st S is Subset of (the_Vertices_of G) holds
( b₃ is AdjGraph of G,S iff b₃ is inducedSubgraph of G,(G .AdjacentSet S) );