let G2 be _Graph; :: thesis: for v being object
for V, E being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds
E = G1 .edgesBetween (V,{v})
let v be object ; :: thesis: for V, E being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds
E = G1 .edgesBetween (V,{v})
let V, E 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 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds
E = 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 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E implies E = G1 .edgesBetween (V,{v}) )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) ; :: thesis: E = G1 .edgesBetween (V,{v})
consider E1 being set such that
A3: ( card V = card E1 & E1 misses the_Edges_of G2 ) and
A4: the_Edges_of G1 = (the_Edges_of G2) \/ E1 and
A5: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E1 & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
A6: E = E1 by A2, A3, A4, XBOOLE_1:71;
A7: E /\ (the_Edges_of G2) = {} by A2, XBOOLE_0:def 7;
for e being object holds
( e in E iff e in G1 .edgesBetween (V,{v}) )

proof

let e be object ; :: thesis: ( e in E iff e in G1 .edgesBetween (V,{v}) )
set x = (the_Source_of G1) . e;
set y = (the_Target_of G1) . e;

hereby :: thesis: ( e in G1 .edgesBetween (V,{v}) implies e in E )

assume A8: e in E ; :: thesis: e in G1 .edgesBetween (V,{v})
then e in the_Edges_of G1 by A2, XBOOLE_0:def 3;
then A9: e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
not e in the_Edges_of G2 by A7, A8, Lm7;

per cases then ( ( (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, A2, A9, 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 A9, 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 A9, GLIB_000:17;
hence e in G1 .edgesBetween (V,{v}) by GLIB_000:def 30; :: thesis: verum

end;

end;

end;

assume e in G1 .edgesBetween (V,{v}) ; :: thesis: e in E
then A10: e SJoins V,{v},G1 by GLIB_000:def 30;
then A11: e in the_Edges_of G1 by GLIB_000:def 15;

per cases ( ( (the_Source_of G1) . e in V & (the_Target_of G1) . e in {v} ) or ( (the_Source_of G1) . e in {v} & (the_Target_of G1) . e in V ) ) by A10, GLIB_000:def 15;

suppose A12: ( (the_Source_of G1) . e in V & (the_Target_of G1) . e in {v} ) ; :: thesis: e in E

then consider e1 being object such that
A13: ( e1 in E1 & e1 Joins (the_Source_of G1) . e,v,G1 ) and
A14: for e2 being object st e2 Joins (the_Source_of G1) . e,v,G1 holds
e1 = e2 by A5;
(the_Target_of G1) . e = v by A12, TARSKI:def 1;
then e Joins (the_Source_of G1) . e,v,G1 by A11, GLIB_000:def 13;
hence e in E by A6, A13, A14; :: thesis: verum

end;

suppose A15: ( (the_Source_of G1) . e in {v} & (the_Target_of G1) . e in V ) ; :: thesis: e in E

then consider e1 being object such that
A16: ( e1 in E1 & e1 Joins (the_Target_of G1) . e,v,G1 ) and
A17: for e2 being object st e2 Joins (the_Target_of G1) . e,v,G1 holds
e1 = e2 by A5;
(the_Source_of G1) . e = v by A15, TARSKI:def 1;
then e Joins (the_Target_of G1) . e,v,G1 by A11, GLIB_000:def 13;
hence e in E by A6, A16, A17; :: thesis: verum

end;

end;

end;

hence E = G1 .edgesBetween (V,{v}) by TARSKI:2; :: thesis: verum