let G2 be _Graph; 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 ; 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 ; 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; ( 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 )
; 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 ;
( e in E iff e in G1 .edgesBetween (V,{v}) )
set x =
(the_Source_of G1) . e;
set y =
(the_Target_of G1) . e;
assume
e in G1 .edgesBetween (
V,
{v})
;
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} )
;
e in Ethen 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;
verum end; suppose A15:
(
(the_Source_of G1) . e in {v} &
(the_Target_of G1) . e in V )
;
e in Ethen 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;
verum end; end;
end;
hence
E = G1 .edgesBetween (V,{v})
by TARSKI:2; verum