theorem :: GLIB_000:155

for G being _Graph
for v being Vertex of G holds
( v is isolated iff ( v .edgesIn() = {} & v .edgesOut() = {} ) ) ;