let G be _Graph; :: thesis:
let v be Vertex of G; :: thesis:

hereby :: thesis:

assume A1: v is isolated ; :: thesis:
assume v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose v in rng (the_Source_of G) ; :: thesis:

then consider e being object such that
A2: ( e in dom (the_Source_of G) & (the_Source_of G) . e = v ) by FUNCT_1:def 3;
e DJoins v,(the_Target_of G) . e,G by A2, GLIB_000:def 14;
hence contradiction by A1, Th26; :: thesis:

end;

suppose v in rng (the_Target_of G) ; :: thesis:

then consider e being object such that
A3: ( e in dom (the_Target_of G) & (the_Target_of G) . e = v ) by FUNCT_1:def 3;
e DJoins (the_Source_of G) . e,v,G by A3, GLIB_000:def 14;
hence contradiction by A1, Th26; :: thesis:

end;

end;

end;

assume A4: not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) ; :: thesis:
assume not v is isolated ; :: thesis:
then v .edgesInOut() <> {} by GLIB_000:def 49;
then consider e being object such that
A5: e in v .edgesInOut() by XBOOLE_0:def 1;
A6: ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) by A5, GLIB_000:61;

per cases ) . e = v or (the_Target_of G) . e = v ) ;

suppose A7: (the_Source_of G) . e = v ; :: thesis:

e in dom (the_Source_of G) by A6, FUNCT_2:def 1;
then v in rng (the_Source_of G) by A7, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3; :: thesis:

end;

suppose A8: (the_Target_of G) . e = v ; :: thesis:

e in dom (the_Target_of G) by A6, FUNCT_2:def 1;
then v in rng (the_Target_of G) by A8, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3; :: thesis:

end;

end;