let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
let v be object ; for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
let V be set ; for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
let G1 be addAdjVertexFromAll of G2,v,V; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) ) )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
then A2:
( the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} & the_Edges_of G1 = (the_Edges_of G2) \/ (V --> (the_Edges_of G2)) & the_Source_of G1 = (the_Source_of G2) +* (pr1 (V,{(the_Edges_of G2)})) & the_Target_of G1 = (the_Target_of G2) +* ((V --> (the_Edges_of G2)) --> v) )
by Def3;
let e1, u be object ; ( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )
thus
not e1 DJoins v,u,G1
( ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )proof
assume
e1 DJoins v,
u,
G1
;
contradiction
then A3:
(
e1 in the_Edges_of G1 &
(the_Source_of G1) . e1 = v &
(the_Target_of G1) . e1 = u )
by GLIB_000:def 14;
not
e1 in the_Edges_of G2
then
e1 in V --> (the_Edges_of G2)
by A2, A3, XBOOLE_0:def 3;
then A5:
e1 in [:V,{(the_Edges_of G2)}:]
;
then A6:
e1 in dom (pr1 (V,{(the_Edges_of G2)}))
by FUNCT_3:def 4;
consider x1,
y1 being
object such that A7:
(
x1 in V &
y1 in {(the_Edges_of G2)} )
and A8:
e1 = [x1,y1]
by A5, ZFMISC_1:def 2;
v =
(pr1 (V,{(the_Edges_of G2)})) . e1
by A2, A3, A6, FUNCT_4:13
.=
(pr1 (V,{(the_Edges_of G2)})) . (
x1,
y1)
by A8, BINOP_1:def 1
.=
x1
by A7, FUNCT_3:def 4
;
hence
contradiction
by A1, A7;
verum
end;
thus
( not u in V implies not e1 DJoins u,v,G1 )
for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2proof
assume A9:
not
u in V
;
not e1 DJoins u,v,G1
assume
e1 DJoins u,
v,
G1
;
contradiction
then A10:
(
e1 in the_Edges_of G1 &
(the_Source_of G1) . e1 = u &
(the_Target_of G1) . e1 = v )
by GLIB_000:def 14;
not
e1 in dom (pr1 (V,{(the_Edges_of G2)}))
proof
assume A11:
e1 in dom (pr1 (V,{(the_Edges_of G2)}))
;
contradiction
then consider x,
y being
object such that A12:
(
x in V &
y in {(the_Edges_of G2)} &
e1 = [x,y] )
by ZFMISC_1:def 2;
u =
(pr1 (V,{(the_Edges_of G2)})) . e1
by A2, A10, A11, FUNCT_4:13
.=
(pr1 (V,{(the_Edges_of G2)})) . (
x,
y)
by A12, BINOP_1:def 1
.=
x
by A12, FUNCT_3:def 4
;
hence
contradiction
by A9, A12;
verum
end;
then
not
e1 in [:V,{(the_Edges_of G2)}:]
by FUNCT_3:def 4;
then A13:
not
e1 in V --> (the_Edges_of G2)
;
then
not
e1 in dom ((V --> (the_Edges_of G2)) --> v)
;
then A14:
(the_Target_of G1) . e1 = (the_Target_of G2) . e1
by A2, FUNCT_4:11;
e1 in the_Edges_of G2
by A2, A10, A13, XBOOLE_0:def 3;
hence
contradiction
by A14, A10, A1, FUNCT_2:5;
verum
end;
let e2 be object ; ( e1 DJoins u,v,G1 & e2 DJoins u,v,G1 implies e1 = e2 )
assume
( e1 DJoins u,v,G1 & e2 DJoins u,v,G1 )
; e1 = e2
then A15:
( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 & (the_Source_of G1) . e1 = u & (the_Source_of G1) . e2 = u & (the_Target_of G1) . e1 = v & (the_Target_of G1) . e2 = v )
by GLIB_000:def 14;
( not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2 )
then
( e1 in V --> (the_Edges_of G2) & e2 in V --> (the_Edges_of G2) )
by A2, A15, XBOOLE_0:def 3;
then A18:
( e1 in [:V,{(the_Edges_of G2)}:] & e2 in [:V,{(the_Edges_of G2)}:] )
;
then A19:
( e1 in dom (pr1 (V,{(the_Edges_of G2)})) & e2 in dom (pr1 (V,{(the_Edges_of G2)})) )
by FUNCT_3:def 4;
consider x1, y1 being object such that
A20:
( x1 in V & y1 in {(the_Edges_of G2)} )
and
A21:
e1 = [x1,y1]
by A18, ZFMISC_1:def 2;
consider x2, y2 being object such that
A22:
( x2 in V & y2 in {(the_Edges_of G2)} )
and
A23:
e2 = [x2,y2]
by A18, ZFMISC_1:def 2;
A24: u =
(pr1 (V,{(the_Edges_of G2)})) . e1
by A2, A15, A19, FUNCT_4:13
.=
(pr1 (V,{(the_Edges_of G2)})) . (x1,y1)
by A21, BINOP_1:def 1
.=
x1
by A20, FUNCT_3:def 4
;
A25: u =
(pr1 (V,{(the_Edges_of G2)})) . e2
by A2, A15, A19, FUNCT_4:13
.=
(pr1 (V,{(the_Edges_of G2)})) . (x2,y2)
by A23, BINOP_1:def 1
.=
x2
by A22, FUNCT_3:def 4
;
( y1 = the_Edges_of G2 & y2 = the_Edges_of G2 )
by A20, A22, TARSKI:def 1;
hence
e1 = e2
by A21, A23, A24, A25; verum