let G2 be _Graph; :: thesis:
let V be set ; :: 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: ( not v1 in V & v1 = v2 ) ; :: thesis:

per cases ;

suppose V c= the_Vertices_of G2 ; :: thesis:

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 = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by Def5;
A3: G2 is Subgraph of G1 by GLIB_006:57;
hence ( v1 is isolated implies v2 is isolated ) by A1, GLIB_000:83; :: thesis:
thus ( v2 is isolated implies v1 is isolated ) :: thesis:

proof

assume A4: v2 is isolated ; :: thesis:
assume not v1 is isolated ; :: thesis:
then v1 .allNeighbors() <> {} by GLIB_000:113;
then consider w being object such that
A5: w in v1 .allNeighbors() by XBOOLE_0:def 1;
consider e being object such that
A6: e Joins v1,w,G1 by A5, GLIB_000:71;

per cases by A1, A6, GLIB_006:72;

suppose A7: e Joins v2,w,G2 ; :: thesis:

w is set by TARSKI:1;
then w in v2 .allNeighbors() by A7, GLIB_000:71;
hence contradiction by A4, GLIB_000:113; :: thesis:

end;

suppose A8: not e in the_Edges_of G2 ; :: thesis:

e in (the_Edges_of G2) \/ E by A2, A6, GLIB_000:def 13;
then A9: e in dom f by A2, A8, XBOOLE_0:5;
then ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A2, FUNCT_4:13;
then v1 = f . e by A6, GLIB_000:def 13;
hence contradiction by A1, A2, A9, FUNCT_1:3; :: thesis:

end;

thus ( v1 is endvertex implies v2 is endvertex ) :: thesis:

proof

assume A10: v1 is endvertex ; :: thesis:
assume not v2 is endvertex ; :: thesis:
then A11: v2 is isolated by A1, A3, A10, GLIB_000:84;
consider e being object such that
A12: ( v1 .edgesInOut() = {e} & not e Joins v1,v1,G1 ) by A10, GLIB_000:def 51;
e in v1 .edgesInOut() by A12, TARSKI:def 1;
then A13: ( e in the_Edges_of G1 & ( (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) ) by GLIB_000:61;

per cases ) . e = v1 or (the_Target_of G1) . e = v1 ) ;

suppose A14: (the_Source_of G1) . e = v1 ; :: thesis:

set w = (the_Target_of G1) . e;
e Joins v1,(the_Target_of G1) . e,G1 by A13, A14, GLIB_000:def 13;
then e Joins v2,(the_Target_of G1) . e,G2 by A1, A12, Th17;
then (the_Target_of G1) . e in v2 .allNeighbors() by GLIB_000:71;
hence contradiction by A11, GLIB_000:113; :: thesis:

end;

suppose A15: (the_Target_of G1) . e = v1 ; :: thesis:

set w = (the_Source_of G1) . e;
e Joins v1,(the_Source_of G1) . e,G1 by A13, A15, GLIB_000:def 13;
then e Joins v2,(the_Source_of G1) . e,G2 by A1, A12, Th17;
then (the_Source_of G1) . e in v2 .allNeighbors() by GLIB_000:71;
hence contradiction by A11, GLIB_000:113; :: thesis:

end;

thus ( v2 is endvertex implies v1 is endvertex ) :: thesis:

proof

assume v2 is endvertex ; :: thesis:
then consider e being object such that
A16: ( v2 .edgesInOut() = {e} & not e Joins v2,v2,G2 ) by GLIB_000:def 51;

now :: thesis:

let e0 be object ; :: thesis:

hereby :: thesis:

assume e0 in v1 .edgesInOut() ; :: thesis:
then A17: ( e0 in the_Edges_of G1 & ( (the_Source_of G1) . e0 = v1 or (the_Target_of G1) . e0 = v1 ) ) by GLIB_000:61;

per cases ) . e0 = v1 or (the_Target_of G1) . e0 = v1 ) ;

suppose A18: (the_Source_of G1) . e0 = v1 ; :: thesis:

set w = (the_Target_of G1) . e0;
A19: e0 Joins v1,(the_Target_of G1) . e0,G1 by A17, A18, GLIB_000:def 13;
e0 in the_Edges_of G2

proof

assume not e0 in the_Edges_of G2 ; :: thesis:
then A20: e0 in dom f by A2, A17, XBOOLE_0:def 3;
then v1 = f . e0 by A2, A17, FUNCT_4:13;
hence contradiction by A1, A2, A20, FUNCT_1:3; :: thesis:

end;

then e0 in v2 .edgesInOut() by A1, A19, GLIB_006:72, GLIB_000:62;
hence e0 = e by A16, TARSKI:def 1; :: thesis:

end;

suppose A21: (the_Target_of G1) . e0 = v1 ; :: thesis:

set w = (the_Source_of G1) . e0;
A22: e0 Joins v1,(the_Source_of G1) . e0,G1 by A17, A21, GLIB_000:def 13;
e0 in the_Edges_of G2

proof

assume not e0 in the_Edges_of G2 ; :: thesis:
then A23: e0 in dom f by A2, A17, XBOOLE_0:def 3;
then v1 = f . e0 by A2, A17, FUNCT_4:13;
hence contradiction by A1, A2, A23, FUNCT_1:3; :: thesis:

end;

then e0 in v2 .edgesInOut() by A1, A22, GLIB_006:72, GLIB_000:62;
hence e0 = e by A16, TARSKI:def 1; :: thesis:

end;

assume e0 = e ; :: thesis:
then e0 in v2 .edgesInOut() by A16, TARSKI:def 1;
hence e0 in v1 .edgesInOut() by A1, A3, GLIB_000:78, TARSKI:def 3; :: thesis:

end;

then A24: v1 .edgesInOut() = {e} by TARSKI:def 1;
e in v2 .edgesInOut() by A16, TARSKI:def 1;
then not e Joins v1,v1,G1 by A1, A16, GLIB_006:72;
hence v1 is endvertex by A24, GLIB_000:def 51; :: thesis:

end;

suppose not V c= the_Vertices_of G2 ; :: thesis:

then G1 == G2 by Def5;
hence ( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) ) by A1, GLIB_000:97; :: thesis:

end;