let G2 be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
let v2 be Vertex of G2; :: thesis: ( not v in the_Vertices_of G2 & v1 = v2 & v2 in V implies ( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 ) )
A1: v is set by TARSKI:1;
assume A2: ( not v in the_Vertices_of G2 & v1 = v2 & v2 in V ) ; :: thesis: ( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: v2 .allNeighbors() c= v1 .allNeighbors() by A2, GLIB_000:82;
consider E being set such that
A5: ( card V = card E & E misses the_Edges_of G2 ) and
the_Edges_of G1 = (the_Edges_of G2) \/ E and
A6: for w1 being object st w1 in V holds
ex e1 being object st
( e1 in E & e1 Joins w1,v,G1 & ( for e2 being object st e2 Joins w1,v,G1 holds
e1 = e2 ) ) by A2, GLIB_007:def 4;
consider e1 being object such that
A7: ( e1 in E & e1 Joins v2,v,G1 ) and
A8: for e2 being object st e2 Joins v2,v,G1 holds
e1 = e2 by A2, A6;
( e1 Joins v1,v,G1 & v is set ) by A2, A7, TARSKI:1;
then {v} c= v1 .allNeighbors() by GLIB_000:71, ZFMISC_1:31;
then A9: (v2 .allNeighbors()) \/ {v} c= v1 .allNeighbors() by A4, XBOOLE_1:8;

now :: thesis: for x being object st x in v1 .allNeighbors() holds
x in (v2 .allNeighbors()) \/ {v}

let x be object ; :: thesis: ( x in v1 .allNeighbors() implies b₁ in (v2 .allNeighbors()) \/ {v} )
assume x in v1 .allNeighbors() ; :: thesis: b₁ in (v2 .allNeighbors()) \/ {v}
then consider e2 being object such that
A10: e2 Joins v1,x,G1 by GLIB_000:71;

per cases ( x <> v or x = v ) ;

suppose x <> v ; :: thesis: b₁ in (v2 .allNeighbors()) \/ {v}

then ( v1 <> v & x <> v ) by A2;
then ( e2 Joins v2,x,G2 & x is set ) by A2, A10, GLIB_007:49, TARSKI:1;
then x in v2 .allNeighbors() by GLIB_000:71;
hence x in (v2 .allNeighbors()) \/ {v} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = v ; :: thesis: b₁ in (v2 .allNeighbors()) \/ {v}

then x in {v} by TARSKI:def 1;
hence x in (v2 .allNeighbors()) \/ {v} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then v1 .allNeighbors() c= (v2 .allNeighbors()) \/ {v} by TARSKI:def 3;
hence v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} by A9, XBOOLE_0:def 10; :: thesis: v1 .degree() = (v2 .degree()) +` 1
A11: ( v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesIn() c= v1 .edgesIn() ) by A2, A3, GLIB_000:78;
A12: e1 is set by TARSKI:1;

per cases ( e1 DJoins v2,v,G1 or e1 DJoins v,v2,G1 ) by A7, GLIB_000:16;

suppose A13: e1 DJoins v2,v,G1 ; :: thesis: v1 .degree() = (v2 .degree()) +` 1

then {e1} c= v1 .edgesOut() by A1, A2, A12, GLIB_000:59, ZFMISC_1:31;
then A14: (v2 .edgesOut()) \/ {e1} c= v1 .edgesOut() by A11, XBOOLE_1:8;

now :: thesis: for e2 being object st e2 in v1 .edgesOut() holds
e2 in (v2 .edgesOut()) \/ {e1}

let e2 be object ; :: thesis: ( e2 in v1 .edgesOut() implies b₁ in (v2 .edgesOut()) \/ {e1} )
assume e2 in v1 .edgesOut() ; :: thesis: b₁ in (v2 .edgesOut()) \/ {e1}
then consider x being set such that
A15: e2 DJoins v1,x,G1 by GLIB_000:59;

per cases ( x <> v or x = v ) ;

suppose x <> v ; :: thesis: b₁ in (v2 .edgesOut()) \/ {e1}

then A16: ( x <> v & v1 <> v & e2 is set ) by A2, TARSKI:1;
then e2 DJoins v1,x,G2 by A2, A15, GLIB_007:def 4;
then e2 in v2 .edgesOut() by A2, A16, GLIB_000:59;
hence e2 in (v2 .edgesOut()) \/ {e1} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = v ; :: thesis: b₁ in (v2 .edgesOut()) \/ {e1}

then e2 Joins v2,v,G1 by A2, A15, GLIB_000:16;
then e1 = e2 by A8;
then e2 in {e1} by TARSKI:def 1;
hence e2 in (v2 .edgesOut()) \/ {e1} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then v1 .edgesOut() c= (v2 .edgesOut()) \/ {e1} by TARSKI:def 3;
then A17: v1 .edgesOut() = (v2 .edgesOut()) \/ {e1} by A14, XBOOLE_0:def 10;

now :: thesis: for e2 being object st e2 in v1 .edgesIn() holds
e2 in v2 .edgesIn()

let e2 be object ; :: thesis: ( e2 in v1 .edgesIn() implies e2 in v2 .edgesIn() )
assume e2 in v1 .edgesIn() ; :: thesis: e2 in v2 .edgesIn()
then consider x being set such that
A18: e2 DJoins x,v1,G1 by GLIB_000:57;
A19: ( e2 is set & v1 <> v ) by A2, TARSKI:1;
x <> v

proof

assume A20: x = v ; :: thesis: contradiction
then e2 Joins v2,v,G1 by A2, A18, GLIB_000:16;
then e1 = e2 by A8;
then x = v1 by A2, A13, A18, GLIB_000:125;
hence contradiction by A2, A20; :: thesis: verum

end;

then e2 DJoins x,v1,G2 by A2, A18, A19, GLIB_007:def 4;
hence e2 in v2 .edgesIn() by A2, A19, GLIB_000:57; :: thesis: verum

end;

then v1 .edgesIn() c= v2 .edgesIn() by TARSKI:def 3;
then A21: v1 .edgesIn() = v2 .edgesIn() by A11, XBOOLE_0:def 10;
not e1 in the_Edges_of G2

proof

assume e1 in the_Edges_of G2 ; :: thesis: contradiction
then e1 in E /\ (the_Edges_of G2) by A7, XBOOLE_0:def 4;
hence contradiction by A5, XBOOLE_0:4; :: thesis: verum

end;

then not e1 in v2 .edgesOut() ;
then A22: {e1} misses v2 .edgesOut() by ZFMISC_1:50;
thus v1 .degree() = (v2 .inDegree()) +` ((card (v2 .edgesOut())) +` (card {e1})) by A17, A21, A22, CARD_2:35
.= (v2 .inDegree()) +` ((v2 .outDegree()) +` 1) by CARD_1:30
.= (v2 .degree()) +` 1 by CARD_2:19 ; :: thesis: verum

end;

suppose A23: e1 DJoins v,v2,G1 ; :: thesis: v1 .degree() = (v2 .degree()) +` 1

then {e1} c= v1 .edgesIn() by A1, A2, A12, GLIB_000:57, ZFMISC_1:31;
then A24: (v2 .edgesIn()) \/ {e1} c= v1 .edgesIn() by A11, XBOOLE_1:8;

now :: thesis: for e2 being object st e2 in v1 .edgesIn() holds
e2 in (v2 .edgesIn()) \/ {e1}

let e2 be object ; :: thesis: ( e2 in v1 .edgesIn() implies b₁ in (v2 .edgesIn()) \/ {e1} )
assume e2 in v1 .edgesIn() ; :: thesis: b₁ in (v2 .edgesIn()) \/ {e1}
then consider x being set such that
A25: e2 DJoins x,v1,G1 by GLIB_000:57;

per cases ( x <> v or x = v ) ;

suppose x <> v ; :: thesis: b₁ in (v2 .edgesIn()) \/ {e1}

then A26: ( x <> v & v1 <> v & e2 is set ) by A2, TARSKI:1;
then e2 DJoins x,v1,G2 by A2, A25, GLIB_007:def 4;
then e2 in v2 .edgesIn() by A2, A26, GLIB_000:57;
hence e2 in (v2 .edgesIn()) \/ {e1} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = v ; :: thesis: b₁ in (v2 .edgesIn()) \/ {e1}

then e2 Joins v2,v,G1 by A2, A25, GLIB_000:16;
then e1 = e2 by A8;
then e2 in {e1} by TARSKI:def 1;
hence e2 in (v2 .edgesIn()) \/ {e1} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then v1 .edgesIn() c= (v2 .edgesIn()) \/ {e1} by TARSKI:def 3;
then A27: v1 .edgesIn() = (v2 .edgesIn()) \/ {e1} by A24, XBOOLE_0:def 10;

now :: thesis: for e2 being object st e2 in v1 .edgesOut() holds
e2 in v2 .edgesOut()

let e2 be object ; :: thesis: ( e2 in v1 .edgesOut() implies e2 in v2 .edgesOut() )
assume e2 in v1 .edgesOut() ; :: thesis: e2 in v2 .edgesOut()
then consider x being set such that
A28: e2 DJoins v1,x,G1 by GLIB_000:59;
A29: ( e2 is set & v1 <> v ) by A2, TARSKI:1;
x <> v

proof

assume A30: x = v ; :: thesis: contradiction
then e2 Joins v2,v,G1 by A2, A28, GLIB_000:16;
then e1 = e2 by A8;
then x = v1 by A2, A23, A28, GLIB_000:125;
hence contradiction by A2, A30; :: thesis: verum

end;

then e2 DJoins v1,x,G2 by A2, A28, A29, GLIB_007:def 4;
hence e2 in v2 .edgesOut() by A2, A29, GLIB_000:59; :: thesis: verum

end;

then v1 .edgesOut() c= v2 .edgesOut() by TARSKI:def 3;
then A31: v1 .edgesOut() = v2 .edgesOut() by A11, XBOOLE_0:def 10;
not e1 in the_Edges_of G2

proof

assume e1 in the_Edges_of G2 ; :: thesis: contradiction
then e1 in E /\ (the_Edges_of G2) by A7, XBOOLE_0:def 4;
hence contradiction by A5, XBOOLE_0:4; :: thesis: verum

end;

then not e1 in v2 .edgesIn() ;
then A32: {e1} misses v2 .edgesIn() by ZFMISC_1:50;
thus v1 .degree() = (v2 .outDegree()) +` ((card (v2 .edgesIn())) +` (card {e1})) by A27, A31, A32, CARD_2:35
.= (v2 .outDegree()) +` ((v2 .inDegree()) +` 1) by CARD_1:30
.= (v2 .degree()) +` 1 by CARD_2:19 ; :: thesis: verum

end;

end;