set R = (rng (the_Source_of G)) \/ (rng (the_Target_of G));
set v = the Element of (the_Vertices_of G) \ ((rng (the_Source_of G)) \/ (rng (the_Target_of G)));
reconsider v = the Element of (the_Vertices_of G) \ ((rng (the_Source_of G)) \/ (rng (the_Target_of G))) as Vertex of G ;
take v ; :: thesis: v is isolated
not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) by XBOOLE_0:def 5;
hence v is isolated by GLIBPRE0:23; :: thesis: verum