let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies ( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) ) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: ( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )
(G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) = {}

proof

assume A2: (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) <> {} ; :: thesis: contradiction
set e = the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2);
A3: the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) in (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) by A2;
the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) in G1 .edgesBetween (V,{v}) by XBOOLE_0:def 4, A2;
then the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) SJoins V,{v},G1 by GLIB_000:def 30;
then consider w being object such that
A4: ( w in V & the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) Joins w,v,G1 ) by GLIB_000:102;
the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) in the_Edges_of G2 by A3, XBOOLE_0:def 4;
then the Element of (G1 .edgesBetween (V,{v})) /\ (the_Edges_of G2) Joins w,v,G2 by A4, GLIB_006:72;
hence contradiction by A1, GLIB_000:13; :: thesis: verum

end;

hence G1 .edgesBetween (V,{v}) misses the_Edges_of G2 by XBOOLE_0:def 7; :: thesis: the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v}))
A5: the_Edges_of G2 c= the_Edges_of G1 by GLIB_006:def 9;
A6: (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) c= the_Edges_of G1 by A5, XBOOLE_1:8;
for e being object st e in the_Edges_of G1 holds
e in (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v}))

proof

let e be object ; :: thesis: ( e in the_Edges_of G1 implies e in (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )
set v1 = (the_Source_of G1) . e;
set v2 = (the_Target_of G1) . e;
assume e in the_Edges_of G1 ; :: thesis: e in (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v}))
then A7: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
( e in the_Edges_of G2 or e in G1 .edgesBetween (V,{v}) )

proof

assume A8: not e in the_Edges_of G2 ; :: thesis: e in G1 .edgesBetween (V,{v})
consider E being set such that
A9: ( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;

per cases ( ( (the_Source_of G1) . e = v & (the_Target_of G1) . e in V ) or ( (the_Target_of G1) . e = v & (the_Source_of G1) . e in V ) ) by A1, A9, A7, A8, Th51;

suppose ( (the_Source_of G1) . e = v & (the_Target_of G1) . e in V ) ; :: thesis: e in G1 .edgesBetween (V,{v})

then ( (the_Source_of G1) . e in {v} & (the_Target_of G1) . e in V ) by TARSKI:def 1;
then e SJoins V,{v},G1 by A7, GLIB_000:17;
hence e in G1 .edgesBetween (V,{v}) by GLIB_000:def 30; :: thesis: verum

end;

suppose ( (the_Target_of G1) . e = v & (the_Source_of G1) . e in V ) ; :: thesis: e in G1 .edgesBetween (V,{v})

then ( (the_Target_of G1) . e in {v} & (the_Source_of G1) . e in V ) by TARSKI:def 1;
then e SJoins V,{v},G1 by A7, GLIB_000:17;
hence e in G1 .edgesBetween (V,{v}) by GLIB_000:def 30; :: thesis: verum

end;

end;

end;

hence e in (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) by XBOOLE_0:def 3; :: thesis: verum

end;

then the_Edges_of G1 c= (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) by TARSKI:def 3;
hence the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) by A6, XBOOLE_0:def 10; :: thesis: verum