let G2 be _Graph; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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 :: thesis: ( ( 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 ; :: thesis: 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
proof
reconsider e3 = e1 as set by TARSKI:1;
assume A4: e1 in the_Edges_of G2 ; :: thesis: contradiction
then (the_Source_of G2) . e3 = v by A3, GLIB_006:def 9;
hence contradiction by A1, A4, FUNCT_2:5; :: thesis: verum
end;
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; :: thesis: verum
end;
thus ( not u in V implies not e1 DJoins u,v,G1 ) :: thesis: for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2
proof
assume A9: not u in V ; :: thesis: not e1 DJoins u,v,G1
assume e1 DJoins u,v,G1 ; :: thesis: 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)})) ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
let e2 be object ; :: thesis: ( e1 DJoins u,v,G1 & e2 DJoins u,v,G1 implies e1 = e2 )
assume ( e1 DJoins u,v,G1 & e2 DJoins u,v,G1 ) ; :: thesis: 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 )
proof
assume ( e1 in the_Edges_of G2 or e2 in the_Edges_of G2 ) ; :: thesis: contradiction
per cases then ( e1 in the_Edges_of G2 or e2 in the_Edges_of G2 ) ;
end;
end;
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; :: thesis: verum