let G3 be _Graph; :: thesis: for v being object
for V being set
for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
let v be object ; :: thesis: for V being set
for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
let V be set ; :: thesis: for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
let v1 be Vertex of G3; :: thesis: for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
let G1 be addAdjVertexAll of G3,v,V \/ {v1}; :: thesis: ( V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V implies ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) ) )
assume that
A1: ( V c= the_Vertices_of G3 & not v in the_Vertices_of G3 ) and
A2: not v1 in V ; :: thesis: ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
set G2 = the removeEdges of G1,(G1 .edgesBetween ({v1},{v}));
A3: V \/ {v1} c= the_Vertices_of G3 by A1, XBOOLE_1:8;
V misses {v1} by A2, ZFMISC_1:50;
then reconsider G2 = the removeEdges of G1,(G1 .edgesBetween ({v1},{v})) as addAdjVertexAll of G3,v,V by A1, A3, Th60;
take G2 ; :: thesis: ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )
reconsider W = {v1} as Subset of (V \/ {v1}) by XBOOLE_1:7;
consider f being Function of W,(G1 .edgesBetween (W,{v})) such that
A4: ( f is one-to-one & f is onto ) and
A5: for w being object st w in W holds
f . w Joins w,v,G1 by A1, A3, Th57;
take f . v1 ; :: thesis: ( not f . v1 in the_Edges_of G2 & ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v ) )
v1 in {v1} by TARSKI:def 1;
then A6: f . v1 Joins v1,v,G1 by A5;
thus not f . v1 in the_Edges_of G2 :: thesis: ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v )

proof

( v1 in {v1} & v in {v} ) by TARSKI:def 1;
then f . v1 SJoins {v1},{v},G1 by A6, GLIB_000:17;
then f . v1 in G1 .edgesBetween ({v1},{v}) by GLIB_000:def 30;
then not f . v1 in (the_Edges_of G1) \ (G1 .edgesBetween ({v1},{v})) by XBOOLE_0:def 5;
hence not f . v1 in the_Edges_of G2 by GLIB_000:53; :: thesis: verum

end;

A7: G1 is Supergraph of G2 by GLIB_006:57;
A8: the_Vertices_of G2 = (the_Vertices_of G3) \/ {v} by A1, Def4;
A9: the_Vertices_of G1 = (the_Vertices_of G3) \/ {v} by A1, A3, Def4;
then A10: the_Vertices_of G1 = the_Vertices_of G2 by A8;
for w being object st w in dom f holds
f . w = f . v1 by TARSKI:def 1;
then f = (dom f) --> (f . v1) by FUNCOP_1:11;
then rng f c= {(f . v1)} by FUNCOP_1:13;
then A11: G1 .edgesBetween (W,{v}) c= {(f . v1)} by A4, FUNCT_2:def 3;
( v1 in {v1} & v in {v} ) by TARSKI:def 1;
then f . v1 SJoins W,{v},G1 by A6, GLIB_000:17;
then f . v1 in G1 .edgesBetween (W,{v}) by GLIB_000:def 30;
then {(f . v1)} c= G1 .edgesBetween (W,{v}) by ZFMISC_1:31;
then A12: G1 .edgesBetween (W,{v}) = {(f . v1)} by A11, XBOOLE_0:def 10;
A13: f . v1 in the_Edges_of G1 by A6, GLIB_000:def 13;
A14: the_Edges_of G2 = (the_Edges_of G1) \ {(f . v1)} by A12, GLIB_000:53;
then A15: the_Edges_of G1 = (the_Edges_of G2) \/ {(f . v1)} by A13, ZFMISC_1:116;
f . v1 in {(f . v1)} by TARSKI:def 1;
then A16: not f . v1 in the_Edges_of G2 by A14, XBOOLE_0:def 5;
A17: v1 in the_Vertices_of G1 by A9, XBOOLE_0:def 3;
v is Vertex of G1 by A1, A3, Th50;
then A18: ( v1 in the_Vertices_of G2 & v in the_Vertices_of G2 ) by A17, A10;
A19: ( G1 is Supergraph of G2 & the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {(f . v1)} ) by A7, A10, A15;

per cases ( f . v1 DJoins v1,v,G1 or f . v1 DJoins v,v1,G1 ) by A6, GLIB_000:16;

suppose A20: f . v1 DJoins v1,v,G1 ; :: thesis: ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v )

A21: dom (the_Source_of G1) = the_Edges_of G1 by GLIB_000:4
.= (the_Edges_of G2) \/ (dom ({(f . v1)} --> v1)) by A15
.= (dom (the_Source_of G2)) \/ (dom ({(f . v1)} --> v1)) by GLIB_000:4
.= (dom (the_Source_of G2)) \/ (dom ((f . v1) .--> v1)) by FUNCOP_1:def 9
.= dom ((the_Source_of G2) +* ((f . v1) .--> v1)) by FUNCT_4:def 1 ;
for e being object st e in dom (the_Source_of G1) holds
(the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v1)) . e

proof

let e be object ; :: thesis: ( e in dom (the_Source_of G1) implies (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v1)) . e )
assume e in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v1)) . e

per cases then ( e in the_Edges_of G2 or e in {(f . v1)} ) by A15, XBOOLE_0:def 3;

suppose A22: e in the_Edges_of G2 ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v1)) . e

then not e in {(f . v1)} by A14, XBOOLE_0:def 5;
then A23: e <> f . v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Source_of G1) . e = (the_Source_of G2) . e1 by A22, GLIB_000:def 32
.= ((the_Source_of G2) +* ((f . v1) .--> v1)) . e by A23, FUNCT_4:83 ; :: thesis: verum

end;

suppose e in {(f . v1)} ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v1)) . e

then A24: e = f . v1 by TARSKI:def 1;
hence (the_Source_of G1) . e = v1 by A20, GLIB_000:def 14
.= ((the_Source_of G2) +* ((f . v1) .--> v1)) . e by A24, FUNCT_4:113 ;
:: thesis: verum

end;

end;

end;

then A25: the_Source_of G1 = (the_Source_of G2) +* ((f . v1) .--> v1) by A21, FUNCT_1:2;
A26: dom (the_Target_of G1) = the_Edges_of G1 by GLIB_000:4
.= (the_Edges_of G2) \/ (dom ({(f . v1)} --> v)) by A15
.= (dom (the_Target_of G2)) \/ (dom ({(f . v1)} --> v)) by GLIB_000:4
.= (dom (the_Target_of G2)) \/ (dom ((f . v1) .--> v)) by FUNCOP_1:def 9
.= dom ((the_Target_of G2) +* ((f . v1) .--> v)) by FUNCT_4:def 1 ;
for e being object st e in dom (the_Target_of G1) holds
(the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v)) . e

proof

let e be object ; :: thesis: ( e in dom (the_Target_of G1) implies (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v)) . e )
assume e in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v)) . e

per cases then ( e in the_Edges_of G2 or e in {(f . v1)} ) by A15, XBOOLE_0:def 3;

suppose A27: e in the_Edges_of G2 ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v)) . e

then not e in {(f . v1)} by A14, XBOOLE_0:def 5;
then A28: e <> f . v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Target_of G1) . e = (the_Target_of G2) . e1 by A27, GLIB_000:def 32
.= ((the_Target_of G2) +* ((f . v1) .--> v)) . e by A28, FUNCT_4:83 ; :: thesis: verum

end;

suppose e in {(f . v1)} ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v)) . e

then A29: e = f . v1 by TARSKI:def 1;
hence (the_Target_of G1) . e = v by A20, GLIB_000:def 14
.= ((the_Target_of G2) +* ((f . v1) .--> v)) . e by A29, FUNCT_4:113 ;
:: thesis: verum

end;

end;

end;

then the_Target_of G1 = (the_Target_of G2) +* ((f . v1) .--> v) by A26, FUNCT_1:2;
hence ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v ) by A16, A25, A19, A18, GLIB_006:def 11; :: thesis: verum

end;

suppose A30: f . v1 DJoins v,v1,G1 ; :: thesis: ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v )

A31: dom (the_Target_of G1) = the_Edges_of G1 by GLIB_000:4
.= (the_Edges_of G2) \/ (dom ({(f . v1)} --> v1)) by A15
.= (dom (the_Target_of G2)) \/ (dom ({(f . v1)} --> v1)) by GLIB_000:4
.= (dom (the_Target_of G2)) \/ (dom ((f . v1) .--> v1)) by FUNCOP_1:def 9
.= dom ((the_Target_of G2) +* ((f . v1) .--> v1)) by FUNCT_4:def 1 ;
for e being object st e in dom (the_Target_of G1) holds
(the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v1)) . e

proof

let e be object ; :: thesis: ( e in dom (the_Target_of G1) implies (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v1)) . e )
assume e in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v1)) . e

per cases then ( e in the_Edges_of G2 or e in {(f . v1)} ) by A15, XBOOLE_0:def 3;

suppose A32: e in the_Edges_of G2 ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v1)) . e

then not e in {(f . v1)} by A14, XBOOLE_0:def 5;
then A33: e <> f . v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Target_of G1) . e = (the_Target_of G2) . e1 by A32, GLIB_000:def 32
.= ((the_Target_of G2) +* ((f . v1) .--> v1)) . e by A33, FUNCT_4:83 ; :: thesis: verum

end;

suppose e in {(f . v1)} ; :: thesis: (the_Target_of G1) . e = ((the_Target_of G2) +* ((f . v1) .--> v1)) . e

then A34: e = f . v1 by TARSKI:def 1;
hence (the_Target_of G1) . e = v1 by A30, GLIB_000:def 14
.= ((the_Target_of G2) +* ((f . v1) .--> v1)) . e by A34, FUNCT_4:113 ;
:: thesis: verum

end;

end;

end;

then A35: the_Target_of G1 = (the_Target_of G2) +* ((f . v1) .--> v1) by A31, FUNCT_1:2;
A36: dom (the_Source_of G1) = the_Edges_of G1 by GLIB_000:4
.= (the_Edges_of G2) \/ (dom ({(f . v1)} --> v)) by A15
.= (dom (the_Source_of G2)) \/ (dom ({(f . v1)} --> v)) by GLIB_000:4
.= (dom (the_Source_of G2)) \/ (dom ((f . v1) .--> v)) by FUNCOP_1:def 9
.= dom ((the_Source_of G2) +* ((f . v1) .--> v)) by FUNCT_4:def 1 ;
for e being object st e in dom (the_Source_of G1) holds
(the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v)) . e

proof

let e be object ; :: thesis: ( e in dom (the_Source_of G1) implies (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v)) . e )
assume e in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v)) . e

per cases then ( e in the_Edges_of G2 or e in {(f . v1)} ) by A15, XBOOLE_0:def 3;

suppose A37: e in the_Edges_of G2 ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v)) . e

then not e in {(f . v1)} by A14, XBOOLE_0:def 5;
then A38: e <> f . v1 by TARSKI:def 1;
reconsider e1 = e as set by TARSKI:1;
thus (the_Source_of G1) . e = (the_Source_of G2) . e1 by A37, GLIB_000:def 32
.= ((the_Source_of G2) +* ((f . v1) .--> v)) . e by A38, FUNCT_4:83 ; :: thesis: verum

end;

suppose e in {(f . v1)} ; :: thesis: (the_Source_of G1) . e = ((the_Source_of G2) +* ((f . v1) .--> v)) . e

then A39: e = f . v1 by TARSKI:def 1;
hence (the_Source_of G1) . e = v by A30, GLIB_000:def 14
.= ((the_Source_of G2) +* ((f . v1) .--> v)) . e by A39, FUNCT_4:113 ;
:: thesis: verum

end;

end;

end;

then the_Source_of G1 = (the_Source_of G2) +* ((f . v1) .--> v) by A36, FUNCT_1:2;
hence ( G1 is addEdge of G2,v,f . v1,v1 or G1 is addEdge of G2,v1,f . v1,v ) by A16, A35, A19, A18, GLIB_006:def 11; :: thesis: verum

end;

end;