let G1, G2 be _Graph; :: thesis: ( G1 is addLoops of G2, {} iff G1 == G2 )

hereby :: thesis: ( G1 == G2 implies G1 is addLoops of G2, {} )

assume A1: G1 is addLoops of G2, {} ; :: thesis: G1 == G2
{} c= the_Vertices_of G2 by XBOOLE_1:2;
then consider E being set , f being one-to-one Function such that
A2: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by A1, Def5;
A3: f = {} by A2;
then A4: E = {} by A2;
A5: the_Source_of G1 = the_Source_of G2 by A2, A3, FUNCT_4:21;
the_Target_of G1 = the_Target_of G2 by A2, A3, FUNCT_4:21;
hence G1 == G2 by A1, A2, A4, A5, Th15, GLIB_000:def 34; :: thesis: verum

end;

assume A6: G1 == G2 ; :: thesis: G1 is addLoops of G2, {}
then A7: G1 is Supergraph of G2 by GLIB_006:59;

now :: thesis: ( {} c= the_Vertices_of G2 & the_Vertices_of G1 = the_Vertices_of G2 & ex E being empty set ex f being empty one-to-one Function st
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) )

thus {} c= the_Vertices_of G2 by XBOOLE_1:2; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & ex E being empty set ex f being empty one-to-one Function st
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) )
thus the_Vertices_of G1 = the_Vertices_of G2 by A6, GLIB_000:def 34; :: thesis: ex E being empty set ex f being empty one-to-one Function st
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
set E = the empty set ;
set f = the empty one-to-one Function;
take E = the empty set ; :: thesis: ex f being empty one-to-one Function st
( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
take f = the empty one-to-one Function; :: thesis: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus E misses the_Edges_of G2 by XBOOLE_1:65; :: thesis: ( the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus the_Edges_of G1 = (the_Edges_of G2) \/ E by A6, GLIB_000:def 34; :: thesis: ( dom f = E & rng f = {} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus ( dom f = E & rng f = {} ) ; :: thesis: ( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus the_Source_of G1 = the_Source_of G2 by A6, GLIB_000:def 34
.= (the_Source_of G2) +* f by FUNCT_4:21 ; :: thesis: the_Target_of G1 = (the_Target_of G2) +* f
thus the_Target_of G1 = the_Target_of G2 by A6, GLIB_000:def 34
.= (the_Target_of G2) +* f by FUNCT_4:21 ; :: thesis: verum

end;

hence G1 is addLoops of G2, {} by A7, Def5; :: thesis: verum