theorem :: GLIB_000:145

for G being _Graph
for v being Vertex of G holds
( v is isolated iff not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) )