theorem :: CHORD:53

for G being _Graph
for x, y being set holds
( x in G .AdjacentSet {y} iff y in G .AdjacentSet {x} )