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 = () \ (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 ) ;
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 = () \ {v1} & the_Edges_of G3 = G1 .edgesBetween (() \ {v1}) ) by ;
A4: ( the_Vertices_of G4 = () \ {v2} & the_Edges_of G4 = G2 .edgesBetween (() \ {v2}) ) by ;
then A5: the_Vertices_of G4 = the_Vertices_of G3 by ;
A6: () \ () = (G1 .edgesBetween ()) \ () by GLIB_000:34
.= the_Edges_of G3 by ;
A7: the_Edges_of G4 = (G2 .edgesBetween ()) \ () by
.= () \ () by GLIB_000:34
.= (() \ (G1 .loops())) \ () by GLIB_000:53
.= (() \ (G1 .loops())) \ (() /\ ()) by GLIB_000:79
.= () \ ((G1 .loops()) \/ (() /\ ())) by XBOOLE_1:41
.= (() \ (() /\ ())) \ (G1 .loops()) by XBOOLE_1:41
.= ((() \ ()) \/ (() \ ())) \ (G1 .loops()) by XBOOLE_1:54
.= (() \/ (G1 .loops())) \ (G1 .loops()) by A1, A6, Th1
.= () \ (G1 .loops()) by XBOOLE_1:40 ;
now :: thesis: for e being object holds
( ( e in () \ (G3 .loops()) implies e in () \ (G1 .loops()) ) & ( e in () \ (G1 .loops()) implies e in () \ (G3 .loops()) ) )
let e be object ; :: thesis: ( ( e in () \ (G3 .loops()) implies e in () \ (G1 .loops()) ) & ( e in () \ (G1 .loops()) implies e in () \ (G3 .loops()) ) )
hereby :: thesis: ( e in () \ (G1 .loops()) implies e in () \ (G3 .loops()) )
assume e in () \ (G3 .loops()) ; :: thesis: e in () \ (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()
proof
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 ;
hence contradiction by A8, Def2; :: thesis: verum
end;
hence e in () \ (G1 .loops()) by ; :: thesis: verum
end;
assume A10: e in () \ (G1 .loops()) ; :: thesis: e in () \ (G3 .loops())
G3 .loops() c= G1 .loops() by Th48;
hence e in () \ (G3 .loops()) by ; :: thesis: verum
end;
then A11: the_Edges_of G4 = () \ (G3 .loops()) by ;
G4 is Subgraph of G1 by GLIB_000:43;
then A12: G4 is Subgraph of G3 by ;
(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 () by GLIB_000:34;
the_Vertices_of G3 c= the_Vertices_of G3 ;
hence G4 is removeLoops of G3 by ; :: thesis: verum
end;
suppose A14: ( G1 is _trivial or not v in the_Vertices_of G1 ) ; :: thesis: G4 is removeLoops of G3
end;
end;