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() = {}

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

hence
v1 is isolated
by GLIB_000:def 49; :: thesis: verum
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;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