let G1 be _Graph; :: thesis: for v being set

for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

let v be set ; :: thesis: for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

let G2 be removeLoops of G1; :: thesis: for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

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

let G4 be removeVertex of G2,v; :: thesis: G4 is removeLoops of G3

A1: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

let v be set ; :: thesis: for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

let G2 be removeLoops of G1; :: thesis: for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

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

let G4 be removeVertex of G2,v; :: thesis: G4 is removeLoops of G3

A1: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ (G1 .loops()) ) by GLIB_000:53;

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 A2:
( not G1 is _trivial & v in the_Vertices_of G1 )
; :: thesis: G4 is removeLoops of G3

then reconsider v1 = v as Vertex of G1 ;

reconsider v2 = v1 as Vertex of G2 by GLIB_000:53;

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

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

then A5: the_Vertices_of G4 = the_Vertices_of G3 by A3, GLIB_000:53;

A6: (the_Edges_of G1) \ (v1 .edgesInOut()) = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by GLIB_000:34

.= the_Edges_of G3 by A3, GLIB_008:1 ;

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

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

.= ((the_Edges_of G1) \ (G1 .loops())) \ (v2 .edgesInOut()) by GLIB_000:53

.= ((the_Edges_of G1) \ (G1 .loops())) \ ((v1 .edgesInOut()) /\ (the_Edges_of G2)) by GLIB_000:79

.= (the_Edges_of G1) \ ((G1 .loops()) \/ ((v1 .edgesInOut()) /\ (the_Edges_of G2))) by XBOOLE_1:41

.= ((the_Edges_of G1) \ ((v1 .edgesInOut()) /\ (the_Edges_of G2))) \ (G1 .loops()) by XBOOLE_1:41

.= (((the_Edges_of G1) \ (v1 .edgesInOut())) \/ ((the_Edges_of G1) \ (the_Edges_of G2))) \ (G1 .loops()) by XBOOLE_1:54

.= ((the_Edges_of G3) \/ (G1 .loops())) \ (G1 .loops()) by A1, A6, Th1

.= (the_Edges_of G3) \ (G1 .loops()) by XBOOLE_1:40 ;

G4 is Subgraph of G1 by GLIB_000:43;

then A12: G4 is Subgraph of G3 by A5, A11, XBOOLE_1:36, GLIB_000:44;

(the_Edges_of G3) \ (G3 .loops()) c= the_Edges_of G3 by XBOOLE_1:36;

then A13: (the_Edges_of G3) \ (G3 .loops()) c= G3 .edgesBetween (the_Vertices_of G3) by GLIB_000:34;

the_Vertices_of G3 c= the_Vertices_of G3 ;

hence G4 is removeLoops of G3 by A5, A11, A12, A13, GLIB_000:def 37; :: thesis: verum

end;reconsider v2 = v1 as Vertex of G2 by GLIB_000:53;

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

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

then A5: the_Vertices_of G4 = the_Vertices_of G3 by A3, GLIB_000:53;

A6: (the_Edges_of G1) \ (v1 .edgesInOut()) = (G1 .edgesBetween (the_Vertices_of G1)) \ (v1 .edgesInOut()) by GLIB_000:34

.= the_Edges_of G3 by A3, GLIB_008:1 ;

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

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

.= ((the_Edges_of G1) \ (G1 .loops())) \ (v2 .edgesInOut()) by GLIB_000:53

.= ((the_Edges_of G1) \ (G1 .loops())) \ ((v1 .edgesInOut()) /\ (the_Edges_of G2)) by GLIB_000:79

.= (the_Edges_of G1) \ ((G1 .loops()) \/ ((v1 .edgesInOut()) /\ (the_Edges_of G2))) by XBOOLE_1:41

.= ((the_Edges_of G1) \ ((v1 .edgesInOut()) /\ (the_Edges_of G2))) \ (G1 .loops()) by XBOOLE_1:41

.= (((the_Edges_of G1) \ (v1 .edgesInOut())) \/ ((the_Edges_of G1) \ (the_Edges_of G2))) \ (G1 .loops()) by XBOOLE_1:54

.= ((the_Edges_of G3) \/ (G1 .loops())) \ (G1 .loops()) by A1, A6, Th1

.= (the_Edges_of G3) \ (G1 .loops()) by XBOOLE_1:40 ;

now :: thesis: for e being object holds

( ( e in (the_Edges_of G3) \ (G3 .loops()) implies e in (the_Edges_of G3) \ (G1 .loops()) ) & ( e in (the_Edges_of G3) \ (G1 .loops()) implies e in (the_Edges_of G3) \ (G3 .loops()) ) )

then A11:
the_Edges_of G4 = (the_Edges_of G3) \ (G3 .loops())
by A7, TARSKI:2;( ( e in (the_Edges_of G3) \ (G3 .loops()) implies e in (the_Edges_of G3) \ (G1 .loops()) ) & ( e in (the_Edges_of G3) \ (G1 .loops()) implies e in (the_Edges_of G3) \ (G3 .loops()) ) )

let e be object ; :: thesis: ( ( e in (the_Edges_of G3) \ (G3 .loops()) implies e in (the_Edges_of G3) \ (G1 .loops()) ) & ( e in (the_Edges_of G3) \ (G1 .loops()) implies e in (the_Edges_of G3) \ (G3 .loops()) ) )

G3 .loops() c= G1 .loops() by Th48;

hence e in (the_Edges_of G3) \ (G3 .loops()) by A10, XBOOLE_1:34, TARSKI:def 3; :: thesis: verum

end;hereby :: thesis: ( e in (the_Edges_of G3) \ (G1 .loops()) implies e in (the_Edges_of G3) \ (G3 .loops()) )

assume A10:
e in (the_Edges_of G3) \ (G1 .loops())
; :: thesis: e in (the_Edges_of G3) \ (G3 .loops())assume
e in (the_Edges_of G3) \ (G3 .loops())
; :: thesis: e in (the_Edges_of G3) \ (G1 .loops())

then A8: ( e in the_Edges_of G3 & not e in G3 .loops() ) by XBOOLE_0:def 5;

not e in G1 .loops()

end;then A8: ( e in the_Edges_of G3 & not e in G3 .loops() ) by XBOOLE_0:def 5;

not e in G1 .loops()

proof

hence
e in (the_Edges_of G3) \ (G1 .loops())
by A8, XBOOLE_0:def 5; :: thesis: verum
assume
e in G1 .loops()
; :: thesis: contradiction

then consider v being object such that

A9: e Joins v,v,G1 by Def2;

( e is set & v is set ) by TARSKI:1;

then e Joins v,v,G3 by A8, A9, GLIB_000:73;

hence contradiction by A8, Def2; :: thesis: verum

end;then consider v being object such that

A9: e Joins v,v,G1 by Def2;

( e is set & v is set ) by TARSKI:1;

then e Joins v,v,G3 by A8, A9, GLIB_000:73;

hence contradiction by A8, Def2; :: thesis: verum

G3 .loops() c= G1 .loops() by Th48;

hence e in (the_Edges_of G3) \ (G3 .loops()) by A10, XBOOLE_1:34, TARSKI:def 3; :: thesis: verum

G4 is Subgraph of G1 by GLIB_000:43;

then A12: G4 is Subgraph of G3 by A5, A11, XBOOLE_1:36, GLIB_000:44;

(the_Edges_of G3) \ (G3 .loops()) c= the_Edges_of G3 by XBOOLE_1:36;

then A13: (the_Edges_of G3) \ (G3 .loops()) c= G3 .edgesBetween (the_Vertices_of G3) by GLIB_000:34;

the_Vertices_of G3 c= the_Vertices_of G3 ;

hence G4 is removeLoops of G3 by A5, A11, A12, A13, GLIB_000:def 37; :: thesis: verum

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

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

G2 == G4 by A1, A14, GLIB_008:8;

then G4 is removeLoops of G1 by Th59;

hence G4 is removeLoops of G3 by A15, Th60; :: thesis: verum

end;G2 == G4 by A1, A14, GLIB_008:8;

then G4 is removeLoops of G1 by Th59;

hence G4 is removeLoops of G3 by A15, Th60; :: thesis: verum