let G1, G2 be _Graph; ( G1 is addLoops of G2, {} iff G1 == G2 )
hereby ( G1 == G2 implies G1 is addLoops of G2, {} )
assume A1:
G1 is
addLoops of
G2,
{}
;
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;
verum
end;
assume A6:
G1 == G2
; G1 is addLoops of G2, {}
then A7:
G1 is Supergraph of G2
by GLIB_006:59;
hence
G1 is addLoops of G2, {}
by A7, Def5; verum