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 (the_Vertices_of G1) ) by GLIB_000:34;

then A2: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E1 ) by A1, GLIB_000:def 37;

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 (the_Vertices_of G1) ) by GLIB_000:34;

then A2: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E1 ) by A1, GLIB_000:def 37;

per cases
( ( not G1 is _trivial & v in the_Vertices_of G1 ) or G1 is _trivial or not v in the_Vertices_of G1 )
;

end;

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 = (the_Vertices_of G1) \ {v1} & the_Edges_of G3 = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) ) by A3, GLIB_000:47;

then A5: the_Edges_of G3 = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by GLIB_008:1

.= (the_Edges_of G1) \ (v1 .edgesInOut()) by GLIB_000:34 ;

A6: ( the_Vertices_of G4 = (the_Vertices_of G2) \ {v2} & the_Edges_of G4 = G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) ) by A3, GLIB_000:47;

then A7: the_Edges_of G4 = (G2 .edgesBetween (the_Vertices_of G2)) \ (v2 .edgesInOut()) by GLIB_008:1

.= (the_Edges_of G2) \ (v2 .edgesInOut()) by GLIB_000:34 ;

set E2 = E1 /\ (the_Edges_of G3);

A8: E1 /\ (the_Edges_of G3) c= the_Edges_of G3 by XBOOLE_1:17;

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 )

then A25: G4 is Subgraph of G3 by A16, A17, GLIB_000:44;

( the_Vertices_of G3 c= the_Vertices_of G3 & the_Edges_of G3 = G3 .edgesBetween (the_Vertices_of G3) ) by GLIB_000:34;

then G4 is inducedSubgraph of G3, the_Vertices_of G3,E2 by A16, A24, A25, GLIB_000:def 37;

hence G4 is removeParallelEdges of G3 by Def7; :: thesis: verum

end;reconsider v2 = v1 as Vertex of G2 by A2;

A4: ( the_Vertices_of G3 = (the_Vertices_of G1) \ {v1} & the_Edges_of G3 = G1 .edgesBetween ((the_Vertices_of G1) \ {v1}) ) by A3, GLIB_000:47;

then A5: the_Edges_of G3 = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by GLIB_008:1

.= (the_Edges_of G1) \ (v1 .edgesInOut()) by GLIB_000:34 ;

A6: ( the_Vertices_of G4 = (the_Vertices_of G2) \ {v2} & the_Edges_of G4 = G2 .edgesBetween ((the_Vertices_of G2) \ {v2}) ) by A3, GLIB_000:47;

then A7: the_Edges_of G4 = (G2 .edgesBetween (the_Vertices_of G2)) \ (v2 .edgesInOut()) by GLIB_008:1

.= (the_Edges_of G2) \ (v2 .edgesInOut()) by GLIB_000:34 ;

set E2 = E1 /\ (the_Edges_of G3);

A8: E1 /\ (the_Edges_of G3) 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 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) )

then reconsider E2 = E1 /\ (the_Edges_of G3) as RepEdgeSelection of G3 by A8, Def5;ex e being object st

( e Joins v,w,G3 & e in E1 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) 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 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) ) )

assume A9: e0 Joins v,w,G3 ; :: thesis: ex e being object st

( e Joins v,w,G3 & e in E1 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) )

A10: ( v is set & w is set ) by TARSKI:1;

then e0 Joins v,w,G1 by A9, GLIB_000:72;

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 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) )

A13: e in the_Edges_of G3

e9 = e ) )

thus e in E1 /\ (the_Edges_of G3) by A11, A13, XBOOLE_0:def 4; :: thesis: for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) implies e9 = e )

assume A15: ( e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) ) ; :: thesis: e9 = e

then ( e9 in E1 & e9 in the_Edges_of G3 ) by XBOOLE_0:def 4;

hence e9 = e by A10, A12, A15, GLIB_000:72; :: thesis: verum

end;( e Joins v,w,G3 & e in E1 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) ) )

assume A9: e0 Joins v,w,G3 ; :: thesis: ex e being object st

( e Joins v,w,G3 & e in E1 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) )

A10: ( v is set & w is set ) by TARSKI:1;

then e0 Joins v,w,G1 by A9, GLIB_000:72;

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 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e ) )

A13: e in the_Edges_of G3

proof

hence
e Joins v,w,G3
by A10, A11, GLIB_000:73; :: thesis: ( e in E1 /\ (the_Edges_of G3) & ( for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds
not e in v1 .edgesInOut()

end;proof

hence
e in the_Edges_of G3
by A5, A11, XBOOLE_0:def 5; :: thesis: verum
assume
e in v1 .edgesInOut()
; :: thesis: contradiction

then ( (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) by GLIB_000:61;

then ( v = v1 or w = v1 ) by A11, GLIB_000:def 13;

then A14: v1 in the_Vertices_of G3 by A9, GLIB_000:13;

v1 in {v1} by TARSKI:def 1;

hence contradiction by A4, A14, XBOOLE_0:def 5; :: thesis: verum

end;then ( (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) by GLIB_000:61;

then ( v = v1 or w = v1 ) by A11, GLIB_000:def 13;

then A14: v1 in the_Vertices_of G3 by A9, GLIB_000:13;

v1 in {v1} by TARSKI:def 1;

hence contradiction by A4, A14, XBOOLE_0:def 5; :: thesis: verum

e9 = e ) )

thus e in E1 /\ (the_Edges_of G3) by A11, A13, XBOOLE_0:def 4; :: thesis: for e9 being object st e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) holds

e9 = e

let e9 be object ; :: thesis: ( e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) implies e9 = e )

assume A15: ( e9 Joins v,w,G3 & e9 in E1 /\ (the_Edges_of G3) ) ; :: thesis: e9 = e

then ( e9 in E1 & e9 in the_Edges_of G3 ) by XBOOLE_0:def 4;

hence e9 = e by A10, A12, A15, GLIB_000:72; :: thesis: verum

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

then A24:
the_Edges_of G4 = E2
by TARSKI:2;
let e be object ; :: thesis: ( e in the_Edges_of G4 iff e in E2 )

then A22: ( e in the_Edges_of G3 & e in E1 ) by XBOOLE_0:def 4;

not e in v2 .edgesInOut()

end;hereby :: thesis: ( e in E2 implies e in the_Edges_of G4 )

assume
e in E2
; :: thesis: e in the_Edges_of G4assume A18:
e in the_Edges_of G4
; :: thesis: e in E2

then A19: e in E1 by A2;

the_Edges_of G4 c= the_Edges_of G1 by A17, GLIB_000:def 32;

then A20: e in the_Edges_of G1 by A18;

not e in v1 .edgesInOut()

hence e in E2 by A19, XBOOLE_0:def 4; :: thesis: verum

end;then A19: e in E1 by A2;

the_Edges_of G4 c= the_Edges_of G1 by A17, GLIB_000:def 32;

then A20: e in the_Edges_of G1 by A18;

not e in v1 .edgesInOut()

proof

then
e in the_Edges_of G3
by A5, A20, XBOOLE_0:def 5;
assume
e in v1 .edgesInOut()
; :: thesis: contradiction

then ( (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) by GLIB_000:61;

then ( e Joins v1,(the_Target_of G1) . e,G1 or e Joins (the_Source_of G1) . e,v1,G1 ) by A20, GLIB_000:def 13;

then ( e Joins v1,(the_Target_of G1) . e,G4 or e Joins (the_Source_of G1) . e,v1,G4 ) by A18, A17, GLIB_000:73;

then A21: v1 in the_Vertices_of G4 by GLIB_000:13;

v1 in {v2} by TARSKI:def 1;

hence contradiction by A6, A21, XBOOLE_0:def 5; :: thesis: verum

end;then ( (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) by GLIB_000:61;

then ( e Joins v1,(the_Target_of G1) . e,G1 or e Joins (the_Source_of G1) . e,v1,G1 ) by A20, GLIB_000:def 13;

then ( e Joins v1,(the_Target_of G1) . e,G4 or e Joins (the_Source_of G1) . e,v1,G4 ) by A18, A17, GLIB_000:73;

then A21: v1 in the_Vertices_of G4 by GLIB_000:13;

v1 in {v2} by TARSKI:def 1;

hence contradiction by A6, A21, XBOOLE_0:def 5; :: thesis: verum

hence e in E2 by A19, XBOOLE_0:def 4; :: thesis: verum

then A22: ( e in the_Edges_of G3 & e in E1 ) by XBOOLE_0:def 4;

not e in v2 .edgesInOut()

proof

hence
e in the_Edges_of G4
by A2, A7, A22, XBOOLE_0:def 5; :: thesis: verum
assume
e in v2 .edgesInOut()
; :: thesis: contradiction

then ( (the_Source_of G2) . e = v2 or (the_Target_of G2) . e = v2 ) by GLIB_000:61;

then ( e Joins v2,(the_Target_of G2) . e,G2 or e Joins (the_Source_of G2) . e,v2,G2 ) by A2, A22, GLIB_000:def 13;

then ( e Joins v2,(the_Target_of G2) . e,G1 or e Joins (the_Source_of G2) . e,v2,G1 ) by GLIB_000:72;

then ( e Joins v2,(the_Target_of G2) . e,G3 or e Joins (the_Source_of G2) . e,v2,G3 ) by A22, GLIB_000:73;

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;then ( (the_Source_of G2) . e = v2 or (the_Target_of G2) . e = v2 ) by GLIB_000:61;

then ( e Joins v2,(the_Target_of G2) . e,G2 or e Joins (the_Source_of G2) . e,v2,G2 ) by A2, A22, GLIB_000:def 13;

then ( e Joins v2,(the_Target_of G2) . e,G1 or e Joins (the_Source_of G2) . e,v2,G1 ) by GLIB_000:72;

then ( e Joins v2,(the_Target_of G2) . e,G3 or e Joins (the_Source_of G2) . e,v2,G3 ) by A22, GLIB_000:73;

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

then A25: G4 is Subgraph of G3 by A16, A17, GLIB_000:44;

( the_Vertices_of G3 c= the_Vertices_of G3 & the_Edges_of G3 = G3 .edgesBetween (the_Vertices_of G3) ) by GLIB_000:34;

then G4 is inducedSubgraph of G3, the_Vertices_of G3,E2 by A16, A24, A25, GLIB_000:def 37;

hence G4 is removeParallelEdges of G3 by Def7; :: thesis: verum

suppose A26:
( G1 is _trivial or not v in the_Vertices_of G1 )
; :: thesis: G4 is removeParallelEdges of G3

then A27:
G1 == G3
by GLIB_008:8;

( G2 is _trivial or not v in the_Vertices_of G2 ) by A26;

then G2 == G4 by GLIB_008:8;

then G4 is removeParallelEdges of G1 by Th93;

hence G4 is removeParallelEdges of G3 by A27, Th91; :: thesis: verum

end;( G2 is _trivial or not v in the_Vertices_of G2 ) by A26;

then G2 == G4 by GLIB_008:8;

then G4 is removeParallelEdges of G1 by Th93;

hence G4 is removeParallelEdges of G3 by A27, Th91; :: thesis: verum