let G1 be _Graph; :: thesis: for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

let G2 be removeParallelEdges of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( v1 is isolated iff v2 is isolated ) )
assume A1: v1 = v2 ; :: thesis: ( v1 is isolated iff v2 is isolated )
hence ( v1 is isolated implies v2 is isolated ) by GLIB_000:83; :: thesis: ( v2 is isolated implies v1 is isolated )
assume v2 is isolated ; :: thesis: v1 is isolated
then A2: v2 .edgesInOut() = {} by GLIB_000:def 49;
v1 .edgesInOut() = {}
proof
assume v1 .edgesInOut() <> {} ; :: thesis: contradiction
then consider e0 being object such that
A3: e0 in v1 .edgesInOut() by XBOOLE_0:def 1;
consider w being Vertex of G1 such that
A4: e0 Joins v1,w,G1 by ;
consider E1 being RepEdgeSelection of G1 such that
A5: G2 is inducedSubgraph of G1, the_Vertices_of G1,E1 by Def7;
consider e1 being object such that
A6: ( e1 Joins v1,w,G1 & e1 in E1 ) and
for e9 being object st e9 Joins v1,w,G1 & e9 in E1 holds
e9 = e1 by ;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween () ) by GLIB_000:34;
then A7: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G2 = E1 ) by ;
then reconsider w = w as Vertex of G2 ;
A8: e1 Joins v2,w,G2 by ;
e1 is set by TARSKI:1;
hence contradiction by A2, A8, GLIB_000:64; :: thesis: verum
end;
hence v1 is isolated by GLIB_000:def 49; :: thesis: verum