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 A3, GLIB_000:64;
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 A4, Def5;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;
then A7: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G2 = E1 ) by A5, GLIB_000:def 37;
then reconsider w = w as Vertex of G2 ;
A8: e1 Joins v2,w,G2 by A1, A6, A7, GLIB_000:73;
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