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 w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = w & v <> w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
let v, w be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,w
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = w & v <> w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = w & v <> w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
let G1 be addEdge of G2,v,e,w; :: thesis: for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = w & v <> w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
let w1 be Vertex of G1; :: thesis: ( not e in the_Edges_of G2 & w1 = w & v <> w implies ( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 ) )
assume A1: ( not e in the_Edges_of G2 & w1 = w & v <> w ) ; :: thesis: ( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
A2: G2 is Subgraph of G1 by GLIB_006:57;

now :: thesis: for f being object holds
( ( f in w1 .edgesIn() implies f in (w .edgesIn()) \/ {e} ) & ( f in (w .edgesIn()) \/ {e} implies f in w1 .edgesIn() ) )

let f be object ; :: thesis: ( ( f in w1 .edgesIn() implies f in (w .edgesIn()) \/ {e} ) & ( f in (w .edgesIn()) \/ {e} implies b₁ in w1 .edgesIn() ) )
thus ( f in w1 .edgesIn() implies f in (w .edgesIn()) \/ {e} ) :: thesis: ( f in (w .edgesIn()) \/ {e} implies b₁ in w1 .edgesIn() )

proof

assume f in w1 .edgesIn() ; :: thesis: f in (w .edgesIn()) \/ {e}
then consider x being set such that
A3: f DJoins x,w1,G1 by GLIB_000:57;

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

suppose A4: f DJoins x,w1,G2 ; :: thesis: f in (w .edgesIn()) \/ {e}

f is set by TARSKI:1;
then f in w .edgesIn() by A1, A4, GLIB_000:57;
hence f in (w .edgesIn()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A5: not f in the_Edges_of G2 ; :: thesis: f in (w .edgesIn()) \/ {e}

f Joins x,w1,G1 by A3, GLIB_000:16;
then f = e by A1, A5, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence f in (w .edgesIn()) \/ {e} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume f in (w .edgesIn()) \/ {e} ; :: thesis: b₁ in w1 .edgesIn()

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

suppose f in w .edgesIn() ; :: thesis: b₁ in w1 .edgesIn()

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

end;

suppose f in {e} ; :: thesis: b₁ in w1 .edgesIn()

then f = e by TARSKI:def 1;
then A6: f DJoins v,w,G1 by A1, GLIB_006:105;
f is set by TARSKI:1;
hence f in w1 .edgesIn() by A1, A6, GLIB_000:57; :: thesis: verum

end;

end;

end;

hence A7: w1 .edgesIn() = (w .edgesIn()) \/ {e} by TARSKI:2; :: thesis: ( w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
not e in w .edgesIn() by A1;
then A8: w .edgesIn() misses {e} by ZFMISC_1:50;
thus A9: w1 .inDegree() = (card (w .edgesIn())) +` (card {e}) by A7, A8, CARD_2:35
.= (w .inDegree()) +` 1 by CARD_1:30 ; :: thesis: ( w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
A10: w .edgesOut() c= w1 .edgesOut() by A1, A2, GLIB_000:78;

now :: thesis: for f being object st f in w1 .edgesOut() holds
f in w .edgesOut()

let f be object ; :: thesis: ( f in w1 .edgesOut() implies f in w .edgesOut() )
assume f in w1 .edgesOut() ; :: thesis: f in w .edgesOut()
then consider x being set such that
A11: f DJoins w1,x,G1 by GLIB_000:59;
f in the_Edges_of G2

proof

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

end;

hence f in w .edgesOut() by A1, A11, GLIB_000:59, GLIB_006:71; :: thesis: verum

end;

then w1 .edgesOut() c= w .edgesOut() by TARSKI:def 3;
hence A14: w1 .edgesOut() = w .edgesOut() by A10, XBOOLE_0:def 10; :: thesis: ( w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
hence A15: w1 .outDegree() = w .outDegree() ; :: thesis: ( w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )
thus w1 .edgesInOut() = (w .edgesInOut()) \/ {e} by A7, A14, XBOOLE_1:4; :: thesis: w1 .degree() = (w .degree()) +` 1
thus w1 .degree() = (w .degree()) +` 1 by A9, A15, CARD_2:19; :: thesis: verum