let G3 be _Graph; :: thesis: for E, V being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V
let E, V be set ; :: thesis: for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V
let G4 be reverseEdgeDirections of G3,E; :: thesis: for G1 being addLoops of G3,V
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V
let G1 be addLoops of G3,V; :: thesis: for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( E c= the_Edges_of G3 implies G2 is addLoops of G4,V )
assume A1: E c= the_Edges_of G3 ; :: thesis: G2 is addLoops of G4,V
A2: the_Vertices_of G2 = the_Vertices_of G1 by GLIB_007:4
.= the_Vertices_of G3 by Th15
.= the_Vertices_of G4 by GLIB_007:4 ;
the_Edges_of G3 c= the_Edges_of G1 by GLIB_006:def 9;
then A3: E c= the_Edges_of G1 by A1, XBOOLE_1:1;
A4: G2 is Supergraph of G4 by A1, GLIBPRE0:50;

per cases ( V c= the_Vertices_of G3 or not V c= the_Vertices_of G3 ) ;

suppose A5: V c= the_Vertices_of G3 ; :: thesis: G2 is addLoops of G4,V

then A6: V c= the_Vertices_of G4 by GLIB_007:4;

now :: thesis: ex D being set ex f being one-to-one Function st
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom f = D & rng f = V & the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )

consider D being set , f being one-to-one Function such that
A7: ( D misses the_Edges_of G3 & the_Edges_of G1 = (the_Edges_of G3) \/ D & dom f = D & rng f = V & the_Source_of G1 = (the_Source_of G3) +* f & the_Target_of G1 = (the_Target_of G3) +* f ) by A5, Def5;
take D = D; :: thesis: ex f being one-to-one Function st
( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom f = D & rng f = V & the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )
take f = f; :: thesis: ( D misses the_Edges_of G4 & the_Edges_of G2 = (the_Edges_of G4) \/ D & dom f = D & rng f = V & the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )
thus D misses the_Edges_of G4 by A7, GLIB_007:4; :: thesis: ( the_Edges_of G2 = (the_Edges_of G4) \/ D & dom f = D & rng f = V & the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )
thus the_Edges_of G2 = the_Edges_of G1 by GLIB_007:4
.= (the_Edges_of G4) \/ D by A7, GLIB_007:4 ; :: thesis: ( dom f = D & rng f = V & the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )
thus ( dom f = D & rng f = V ) by A7; :: thesis: ( the_Source_of G2 = (the_Source_of G4) +* f & the_Target_of G2 = (the_Target_of G4) +* f )
E = (the_Edges_of G3) /\ E by A1, XBOOLE_1:28;
then A8: dom f misses (the_Edges_of G3) /\ E by A1, A7, XBOOLE_1:63;
then dom f misses (dom (the_Source_of G3)) /\ E by FUNCT_2:def 1;
then A9: dom f misses dom ((the_Source_of G3) | E) by RELAT_1:61;
dom f misses (dom (the_Target_of G3)) /\ E by A8, FUNCT_2:def 1;
then A10: dom f misses dom ((the_Target_of G3) | E) by RELAT_1:61;
A11: (the_Source_of G1) | E = ((the_Source_of G1) | (the_Edges_of G3)) | E by A1, RELAT_1:74
.= (the_Source_of G3) | E by GLIB_006:69 ;
A12: (the_Target_of G1) | E = ((the_Target_of G1) | (the_Edges_of G3)) | E by A1, RELAT_1:74
.= (the_Target_of G3) | E by GLIB_006:69 ;
thus the_Source_of G2 = (the_Source_of G1) +* ((the_Target_of G1) | E) by A3, GLIB_007:def 1
.= (the_Source_of G3) +* (f +* ((the_Target_of G3) | E)) by A7, A12, FUNCT_4:14
.= (the_Source_of G3) +* (((the_Target_of G3) | E) +* f) by A10, FUNCT_4:35
.= ((the_Source_of G3) +* ((the_Target_of G3) | E)) +* f by FUNCT_4:14
.= (the_Source_of G4) +* f by A1, GLIB_007:def 1 ; :: thesis: the_Target_of G2 = (the_Target_of G4) +* f
thus the_Target_of G2 = (the_Target_of G1) +* ((the_Source_of G1) | E) by A3, GLIB_007:def 1
.= (the_Target_of G3) +* (f +* ((the_Source_of G3) | E)) by A7, A11, FUNCT_4:14
.= (the_Target_of G3) +* (((the_Source_of G3) | E) +* f) by A9, FUNCT_4:35
.= ((the_Target_of G3) +* ((the_Source_of G3) | E)) +* f by FUNCT_4:14
.= (the_Target_of G4) +* f by A1, GLIB_007:def 1 ; :: thesis: verum

end;

hence G2 is addLoops of G4,V by A2, A4, A6, Def5; :: thesis: verum

end;

suppose not V c= the_Vertices_of G3 ; :: thesis: G2 is addLoops of G4,V

then A13: ( G1 == G3 & not V c= the_Vertices_of G4 ) by Def5, GLIB_007:4;
G3 is reverseEdgeDirections of G4,E by GLIB_007:3;
then G1 is reverseEdgeDirections of G4,E by A13, GLIB_007:2;
then G4 is reverseEdgeDirections of G1,E by GLIB_007:3;
then G2 == G4 by GLIB_007:1;
hence G2 is addLoops of G4,V by A4, A13, Def5; :: thesis: verum

end;

end;