let G2 be _Graph; :: thesis: for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v & v <> w holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let v, w be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v & v <> w holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v & v <> w holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let G1 be addEdge of G2,v,e,w; :: thesis: for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v & v <> w holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
let v1 be Vertex of G1; :: thesis: ( not e in the_Edges_of G2 & v1 = v & v <> w implies ( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 ) )
assume A1: ( not e in the_Edges_of G2 & v1 = v & v <> w ) ; :: thesis: ( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
A2: G2 is Subgraph of G1 by GLIB_006:57;
A3: v .edgesIn() c= v1 .edgesIn() by A1, A2, GLIB_000:78;

now :: thesis: for f being object st f in v1 .edgesIn() holds
f in v .edgesIn()

let f be object ; :: thesis: ( f in v1 .edgesIn() implies f in v .edgesIn() )
assume f in v1 .edgesIn() ; :: thesis: f in v .edgesIn()
then consider x being set such that
A4: f DJoins x,v1,G1 by GLIB_000:57;
f in the_Edges_of G2

proof

assume A6: not f in the_Edges_of G2 ; :: thesis: contradiction
f Joins x,v1,G1 by A4, GLIB_000:16;
then f = e by A1, A6, GLIB_006:106;
then f DJoins v,w,G1 by A1, GLIB_006:105;
hence contradiction by A1, A4, GLIB_000:125; :: thesis: verum

end;

hence f in v .edgesIn() by A1, A4, GLIB_006:71, GLIB_000:57; :: thesis: verum

end;

then v1 .edgesIn() c= v .edgesIn() by TARSKI:def 3;
hence A7: v1 .edgesIn() = v .edgesIn() by A3, XBOOLE_0:def 10; :: thesis: ( v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
hence A8: v1 .inDegree() = v .inDegree() ; :: thesis: ( v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )

now :: thesis: for f being object holds
( ( f in v1 .edgesOut() implies f in (v .edgesOut()) \/ {e} ) & ( f in (v .edgesOut()) \/ {e} implies f in v1 .edgesOut() ) )

let f be object ; :: thesis: ( ( f in v1 .edgesOut() implies f in (v .edgesOut()) \/ {e} ) & ( f in (v .edgesOut()) \/ {e} implies b₁ in v1 .edgesOut() ) )
thus ( f in v1 .edgesOut() implies f in (v .edgesOut()) \/ {e} ) :: thesis: ( f in (v .edgesOut()) \/ {e} implies b₁ in v1 .edgesOut() )

proof

assume f in v1 .edgesOut() ; :: thesis: f in (v .edgesOut()) \/ {e}
then consider x being set such that
A9: f DJoins v1,x,G1 by GLIB_000:59;

per cases ( f DJoins v1,x,G2 or not f in the_Edges_of G2 ) by A9, GLIB_006:71;

suppose A10: f DJoins v1,x,G2 ; :: thesis: f in (v .edgesOut()) \/ {e}

f is set by TARSKI:1;
then f in v .edgesOut() by A1, A10, GLIB_000:59;
hence f in (v .edgesOut()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A11: not f in the_Edges_of G2 ; :: thesis: f in (v .edgesOut()) \/ {e}

f Joins x,v1,G1 by A9, GLIB_000:16;
then f = e by A1, A11, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence f in (v .edgesOut()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume f in (v .edgesOut()) \/ {e} ; :: thesis: b₁ in v1 .edgesOut()

per cases then ( f in v .edgesOut() or f in {e} ) by XBOOLE_0:def 3;

suppose f in v .edgesOut() ; :: thesis: b₁ in v1 .edgesOut()

hence f in v1 .edgesOut() by A1, A2, GLIB_000:78, TARSKI:def 3; :: thesis: verum

end;

suppose f in {e} ; :: thesis: b₁ in v1 .edgesOut()

then ( f = e & f is set ) by TARSKI:def 1;
hence f in v1 .edgesOut() by A1, GLIB_000:59, GLIB_006:105; :: thesis: verum

end;

end;

end;

hence A12: v1 .edgesOut() = (v .edgesOut()) \/ {e} by TARSKI:2; :: thesis: ( v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
not e in v .edgesOut() by A1;
then A13: v .edgesOut() misses {e} by ZFMISC_1:50;
thus A14: v1 .outDegree() = (card (v .edgesOut())) +` (card {e}) by A12, A13, CARD_2:35
.= (v .outDegree()) +` 1 by CARD_1:30 ; :: thesis: ( v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )
thus v1 .edgesInOut() = (v .edgesInOut()) \/ {e} by A7, A12, XBOOLE_1:4; :: thesis: v1 .degree() = (v .degree()) +` 1
thus v1 .degree() = (v .degree()) +` 1 by A8, A14, CARD_2:19; :: thesis: verum