let G1 be _Graph; :: thesis: for v being set
for G2 being removeParallelEdges of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

let v be set ; :: thesis: for G2 being removeParallelEdges of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

let G2 be removeParallelEdges of G1; :: thesis: for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

let G3 be removeVertex of G1,v; :: thesis: for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3
let G4 be removeVertex of G2,v; :: thesis: G4 is removeParallelEdges of G3
consider E1 being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E1 by Def7;
( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween () ) by GLIB_000:34;
then A2: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E1 ) by ;
per cases ( ( not G1 is _trivial & v in the_Vertices_of G1 ) or G1 is _trivial or not v in the_Vertices_of G1 ) ;
suppose A3: ( not G1 is _trivial & v in the_Vertices_of G1 ) ; :: thesis: G4 is removeParallelEdges of G3
then reconsider v1 = v as Vertex of G1 ;
reconsider v2 = v1 as Vertex of G2 by A2;
A4: ( the_Vertices_of G3 = () \ {v1} & the_Edges_of G3 = G1 .edgesBetween (() \ {v1}) ) by ;
then A5: the_Edges_of G3 = (G1 .edgesBetween ()) \ () by GLIB_008:1
.= () \ () by GLIB_000:34 ;
A6: ( the_Vertices_of G4 = () \ {v2} & the_Edges_of G4 = G2 .edgesBetween (() \ {v2}) ) by ;
then A7: the_Edges_of G4 = (G2 .edgesBetween ()) \ () by GLIB_008:1
.= () \ () by GLIB_000:34 ;
set E2 = E1 /\ ();
A8: E1 /\ () c= the_Edges_of G3 by XBOOLE_1:17;
now :: thesis: for v, w, e0 being object st e0 Joins v,w,G3 holds
ex e being object st
( e Joins v,w,G3 & e in E1 /\ () & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e ) )
let v, w, e0 be object ; :: thesis: ( e0 Joins v,w,G3 implies ex e being object st
( e Joins v,w,G3 & e in E1 /\ () & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e ) ) )

assume A9: e0 Joins v,w,G3 ; :: thesis: ex e being object st
( e Joins v,w,G3 & e in E1 /\ () & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e ) )

A10: ( v is set & w is set ) by TARSKI:1;
then e0 Joins v,w,G1 by ;
then consider e being object such that
A11: ( e Joins v,w,G1 & e in E1 ) and
A12: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds
e9 = e by Def5;
take e = e; :: thesis: ( e Joins v,w,G3 & e in E1 /\ () & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e ) )

A13: e in the_Edges_of G3 hence e Joins v,w,G3 by ; :: thesis: ( e in E1 /\ () & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e ) )

thus e in E1 /\ () by ; :: thesis: for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ () holds
e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G3 & e9 in E1 /\ () implies e9 = e )
assume A15: ( e9 Joins v,w,G3 & e9 in E1 /\ () ) ; :: thesis: e9 = e
then ( e9 in E1 & e9 in the_Edges_of G3 ) by XBOOLE_0:def 4;
hence e9 = e by ; :: thesis: verum
end;
then reconsider E2 = E1 /\ () as RepEdgeSelection of G3 by ;
A16: the_Vertices_of G4 = the_Vertices_of G3 by A2, A4, A6;
A17: G4 is Subgraph of G1 by GLIB_000:43;
for e being object holds
( e in the_Edges_of G4 iff e in E2 )
proof
let e be object ; :: thesis: ( e in the_Edges_of G4 iff e in E2 )
hereby :: thesis: ( e in E2 implies e in the_Edges_of G4 ) end;
assume e in E2 ; :: thesis:
then A22: ( e in the_Edges_of G3 & e in E1 ) by XBOOLE_0:def 4;
not e in v2 .edgesInOut()
proof
assume e in v2 .edgesInOut() ; :: thesis: contradiction
then ( (the_Source_of G2) . e = v2 or () . e = v2 ) by GLIB_000:61;
then ( e Joins v2,() . e,G2 or e Joins () . e,v2,G2 ) by ;
then ( e Joins v2,() . e,G1 or e Joins () . e,v2,G1 ) by GLIB_000:72;
then ( e Joins v2,() . e,G3 or e Joins () . e,v2,G3 ) by ;
then A23: v2 in the_Vertices_of G3 by GLIB_000:13;
v2 in {v1} by TARSKI:def 1;
hence contradiction by A4, A23, XBOOLE_0:def 5; :: thesis: verum
end;
hence e in the_Edges_of G4 by ; :: thesis: verum
end;
then A24: the_Edges_of G4 = E2 by TARSKI:2;
then A25: G4 is Subgraph of G3 by ;
( the_Vertices_of G3 c= the_Vertices_of G3 & the_Edges_of G3 = G3 .edgesBetween () ) by GLIB_000:34;
then G4 is inducedSubgraph of G3, the_Vertices_of G3,E2 by ;
hence G4 is removeParallelEdges of G3 by Def7; :: thesis: verum
end;
suppose A26: ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis: G4 is removeParallelEdges of G3
end;
end;