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 holds
( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )
let v, w be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )
let G1 be addEdge of G2,v,e,w; :: thesis: ( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )
assume A1: v <> w ; :: thesis: ( G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )

per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;

suppose A2: not e in the_Edges_of G2 ; :: thesis: ( G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )

then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
then reconsider v9 = v, w9 = w as Vertex of G1 ;
consider v1 being Vertex of G1 such that
A4: v1 .inDegree() = G1 .minInDegree() and
A5: for w1 being Vertex of G1 holds v1 .inDegree() c= w1 .inDegree() by Th37;
reconsider v4 = v1 as Vertex of G2 by A3;
consider v2 being Vertex of G2 such that
A6: v2 .inDegree() = G2 .minInDegree() and
A7: for w2 being Vertex of G2 holds v2 .inDegree() c= w2 .inDegree() by Th37;
reconsider v3 = v2 as Vertex of G1 by A3;
A8: ( v2 .inDegree() c= v4 .inDegree() & v1 .inDegree() c= v3 .inDegree() ) by A5, A7;
G2 is Subgraph of G1 by GLIB_006:57;
then ( v4 .inDegree() c= v1 .inDegree() & v2 .inDegree() c= v3 .inDegree() ) by CARD_1:11, GLIB_000:78;
then A9: ( v2 .inDegree() c= v1 .inDegree() & v4 .inDegree() c= v3 .inDegree() ) by A8, XBOOLE_1:1;
assume G1 .minInDegree() <> G2 .minInDegree() ; :: thesis: G1 .minInDegree() = (w .inDegree()) +` 1
then A10: v1 .inDegree() <> v2 .inDegree() by A4, A6;
then A11: (v2 .inDegree()) +` 1 c= v1 .inDegree() by A9, Lm1;
A12: v2 = w

proof

assume A13: v2 <> w ; :: thesis: contradiction
A14: v2 .inDegree() = v3 .inDegree()

proof

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

suppose v2 = v ; :: thesis: v2 .inDegree() = v3 .inDegree()

hence v2 .inDegree() = v3 .inDegree() by A1, A2, GLIBPRE0:47; :: thesis: verum

end;

suppose v2 <> v ; :: thesis: v2 .inDegree() = v3 .inDegree()

hence v2 .inDegree() = v3 .inDegree() by A13, GLIBPRE0:46; :: thesis: verum

end;

end;

end;

then A15: (v3 .inDegree()) +` 1 c= v3 .inDegree() by A8, A11, XBOOLE_1:1;
v3 .inDegree() c= (v3 .inDegree()) +` 1 by CARD_2:94;
then v3 .inDegree() = (v3 .inDegree()) +` 1 by A15, XBOOLE_0:def 10;
hence contradiction by A8, A10, A11, A14, XBOOLE_0:def 10; :: thesis: verum

end;

then v3 .inDegree() = (v2 .inDegree()) +` 1 by A1, A2, GLIBPRE0:48;
hence G1 .minInDegree() = (w .inDegree()) +` 1 by A4, A8, A11, A12, XBOOLE_0:def 10; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: ( G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )

then G1 == G2 by GLIB_006:def 11;
hence ( G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 ) by Th62; :: thesis: verum

end;

end;