let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let G1 be addAdjVertexAll of G2,v; :: thesis:
assume A1: not v in the_Vertices_of G2 ; :: thesis:
then reconsider v9 = v as Vertex of G1 by GLIB_007:50;
consider v0 being Vertex of G2 such that
A2: G2 .minDegree() = v0 .degree() and
A3: for w0 being Vertex of G2 holds v0 .degree() c= w0 .degree() by Th36;
A4: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, GLIB_007:def 4;
then reconsider v1 = v0 as Vertex of G1 by XBOOLE_0:def 3;
A5: the_Vertices_of G2 c= the_Vertices_of G2 ;
A6: v9 .degree() = G2 .order() by A1, GLIBPRE0:57;
A7: v1 .degree() = (v0 .degree()) +` 1 by A1, A5, GLIBPRE0:59;

per cases ) +` 1 c= v9 .degree() or v9 .degree() c= (v0 .degree()) +` 1 ) ;

suppose A8: (v0 .degree()) +` 1 c= v9 .degree() ; :: thesis:

then A9: ((G2 .minDegree()) +` 1) /\ (G2 .order()) = (v0 .degree()) +` 1 by A2, A6, XBOOLE_1:28;

now :: thesis:

let w be Vertex of G1; :: thesis:

per cases by A4, XBOOLE_0:def 3;

suppose w in the_Vertices_of G2 ; :: thesis:

then reconsider w0 = w as Vertex of G2 ;
( v0 .degree() c= w0 .degree() & 1 c= 1 ) by A3;
then v1 .degree() c= (w0 .degree()) +` 1 by A7, CARD_2:83;
hence v1 .degree() c= w .degree() by A1, A5, GLIBPRE0:59; :: thesis:

end;

suppose w in {v} ; :: thesis:

hence v1 .degree() c= w .degree() by A7, A8, TARSKI:def 1; :: thesis:

end;

end;

end;

hence G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order()) by A7, A9, Th36; :: thesis:

end;

suppose A10: v9 .degree() c= (v0 .degree()) +` 1 ; :: thesis:

then A11: ((G2 .minDegree()) +` 1) /\ (G2 .order()) = v9 .degree() by A2, A6, XBOOLE_1:28;

now :: thesis:

let w be Vertex of G1; :: thesis:

per cases by A4, XBOOLE_0:def 3;

suppose w in the_Vertices_of G2 ; :: thesis:

then reconsider w0 = w as Vertex of G2 ;
( v0 .degree() c= w0 .degree() & 1 c= 1 ) by A3;
then (v0 .degree()) +` 1 c= (w0 .degree()) +` 1 by CARD_2:83;
then v9 .degree() c= (w0 .degree()) +` 1 by A10, XBOOLE_1:1;
hence v9 .degree() c= w .degree() by A1, A5, GLIBPRE0:59; :: thesis:

end;

suppose w in {v} ; :: thesis:

hence v9 .degree() c= w .degree() by TARSKI:def 1; :: thesis:

end;

end;

end;

hence G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order()) by A11, Th36; :: thesis:

end;

end;