theorem :: CHORD:56

for G being loopless _Graph
for u being Vertex of G holds
( G .AdjacentSet {u} = {} iff u is isolated )