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 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .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 holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )
let G1 be addEdge of G2,v,e,w; :: thesis: ( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )
assume A1: v <> w ; :: thesis: ( G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 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 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 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 .degree() = G1 .minDegree() and
A5: for w1 being Vertex of G1 holds v1 .degree() c= w1 .degree() by Th36;
reconsider v4 = v1 as Vertex of G2 by A3;
consider v2 being Vertex of G2 such that
A6: v2 .degree() = G2 .minDegree() and
A7: for w2 being Vertex of G2 holds v2 .degree() c= w2 .degree() by Th36;
reconsider v3 = v2 as Vertex of G1 by A3;
A8: ( v2 .degree() c= v4 .degree() & v1 .degree() c= v3 .degree() ) by A5, A7;
A9: G2 is Subgraph of G1 by GLIB_006:57;
then A10: ( v4 .inDegree() c= v1 .inDegree() & v2 .inDegree() c= v3 .inDegree() ) by GLIB_000:78, CARD_1:11;
( v4 .outDegree() c= v1 .outDegree() & v2 .outDegree() c= v3 .outDegree() ) by A9, GLIB_000:78, CARD_1:11;
then ( v4 .degree() c= v1 .degree() & v2 .degree() c= v3 .degree() ) by A10, CARD_2:83;
then A11: ( v2 .degree() c= v1 .degree() & v4 .degree() c= v3 .degree() ) by A8, XBOOLE_1:1;
assume G1 .minDegree() <> G2 .minDegree() ; :: thesis: G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1
then A12: v1 .degree() <> v2 .degree() by A4, A6;
then A13: (v2 .degree()) +` 1 c= v1 .degree() by A11, Lm1;
A14: ( v2 = v or v2 = w )

proof

assume ( v2 <> v & v2 <> w ) ; :: thesis: contradiction
then A15: v2 .degree() = v3 .degree() by GLIBPRE0:46;
then A16: (v3 .degree()) +` 1 c= v3 .degree() by A8, A13, XBOOLE_1:1;
v3 .degree() c= (v3 .degree()) +` 1 by CARD_2:94;
then v3 .degree() = (v3 .degree()) +` 1 by A16, XBOOLE_0:def 10;
hence contradiction by A8, A12, A13, A15, XBOOLE_0:def 10; :: thesis: verum

end;

then v3 .degree() = (v2 .degree()) +` 1 by A1, A2, GLIBPRE0:48, GLIBPRE0:47;
then v1 .degree() = (v2 .degree()) +` 1 by A8, A13, XBOOLE_0:def 10;
hence G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 by A4, A7, A14, XBOOLE_1:28; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: ( G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )

then G1 == G2 by GLIB_006:def 11;
hence ( G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 ) by Th62; :: thesis: verum

end;

end;