let G2 be _Graph; :: thesis:
let V be Subset of (the_Vertices_of G2); :: thesis:
let G1 be addLoops of G2,V; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & v1 in V ) ; :: thesis:
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 ) and
A3: ( dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f ) and
A4: the_Target_of G1 = (the_Target_of G2) +* f by Def5;
consider e being object such that
A5: ( e in dom f & f . e = v1 ) by A1, A3, FUNCT_1:def 3;
take e ; :: thesis:
A6: e in the_Edges_of G1 by A2, A3, A5, XBOOLE_0:def 3;
A7: (the_Source_of G1) . e = v1 by A3, A5, FUNCT_4:13;
(the_Target_of G1) . e = v1 by A4, A5, FUNCT_4:13;
hence A8: e DJoins v1,v1,G1 by A6, A7, GLIB_000:def 14; :: thesis:
thus not e in the_Edges_of G2 :: thesis:

proof

assume e in the_Edges_of G2 ; :: thesis:
then e in E /\ (the_Edges_of G2) by A3, A5, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 7; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in v1 .edgesIn() ; :: thesis:
then consider w being set such that
A9: x DJoins w,v1,G1 by GLIB_000:57;

per cases by A9, GLIB_006:71;

suppose A10: x DJoins w,v1,G2 ; :: thesis:

x is set by TARSKI:1;
then x in v2 .edgesIn() by A1, A10, GLIB_000:57;
hence x in (v2 .edgesIn()) \/ {e} by XBOOLE_0:def 3; :: thesis:

end;

suppose A11: not x in the_Edges_of G2 ; :: thesis:

x in the_Edges_of G1 by A9, GLIB_000:def 14;
then A12: x in E by A2, A11, XBOOLE_0:def 3;
f . x = (the_Target_of G1) . x by A3, A4, A12, FUNCT_4:13
.= v1 by A9, GLIB_000:def 14 ;
then x = e by A3, A5, A12, FUNCT_1:def 4;
then x in {e} by TARSKI:def 1;
hence x in (v2 .edgesIn()) \/ {e} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (v2 .edgesIn()) \/ {e} ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A13: x in v2 .edgesIn() ; :: thesis:

G2 is Subgraph of G1 by GLIB_006:57;
then v2 .edgesIn() c= v1 .edgesIn() by A1, GLIB_000:78;
hence x in v1 .edgesIn() by A13; :: thesis:

end;

suppose x in {e} ; :: thesis:

then ( x = e & e is set ) by TARSKI:def 1;
hence x in v1 .edgesIn() by A8, GLIB_000:57; :: thesis:

end;

end;

end;

hence A14: v1 .edgesIn() = (v2 .edgesIn()) \/ {e} by TARSKI:2; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in v1 .edgesOut() ; :: thesis:
then consider w being set such that
A15: x DJoins v1,w,G1 by GLIB_000:59;

per cases by A15, GLIB_006:71;

suppose A16: x DJoins v1,w,G2 ; :: thesis:

x is set by TARSKI:1;
then x in v2 .edgesOut() by A1, A16, GLIB_000:59;
hence x in (v2 .edgesOut()) \/ {e} by XBOOLE_0:def 3; :: thesis:

end;

suppose A17: not x in the_Edges_of G2 ; :: thesis:

x in the_Edges_of G1 by A15, GLIB_000:def 14;
then A18: x in E by A2, A17, XBOOLE_0:def 3;
f . x = (the_Source_of G1) . x by A3, A18, FUNCT_4:13
.= v1 by A15, GLIB_000:def 14 ;
then x = e by A3, A5, A18, FUNCT_1:def 4;
then x in {e} by TARSKI:def 1;
hence x in (v2 .edgesOut()) \/ {e} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume x in (v2 .edgesOut()) \/ {e} ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose A19: x in v2 .edgesOut() ; :: thesis:

G2 is Subgraph of G1 by GLIB_006:57;
then v2 .edgesOut() c= v1 .edgesOut() by A1, GLIB_000:78;
hence x in v1 .edgesOut() by A19; :: thesis:

end;

suppose x in {e} ; :: thesis:

then ( x = e & e is set ) by TARSKI:def 1;
hence x in v1 .edgesOut() by A8, GLIB_000:59; :: thesis:

end;

end;

end;

hence A20: v1 .edgesOut() = (v2 .edgesOut()) \/ {e} by TARSKI:2; :: thesis:
thus v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} by A14, A20, XBOOLE_1:5; :: thesis: