let G2 be _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())
let G1 be addAdjVertexAll of G2,v; :: thesis: ( not v in the_Vertices_of G2 implies G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order()) )
assume A1: not v in the_Vertices_of G2 ; :: thesis: G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())
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:55;
A7: v1 .degree() = (v0 .degree()) +` 1 by A1, A5, GLIBPRE0:57;

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

suppose A8: (v0 .degree()) +` 1 c= v9 .degree() ; :: thesis: G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())

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

now :: thesis: for w being Vertex of G1 holds v1 .degree() c= w .degree()

let w be Vertex of G1; :: thesis: v1 .degree() c= b₁ .degree()

per cases ( w in the_Vertices_of G2 or w in {v} ) by A4, XBOOLE_0:def 3;

suppose w in the_Vertices_of G2 ; :: thesis: v1 .degree() c= b₁ .degree()

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:57; :: thesis: verum

end;

suppose w in {v} ; :: thesis: v1 .degree() c= b₁ .degree()

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

end;

end;

end;

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

end;

suppose A10: v9 .degree() c= (v0 .degree()) +` 1 ; :: thesis: G1 .minDegree() = ((G2 .minDegree()) +` 1) /\ (G2 .order())

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

now :: thesis: for w being Vertex of G1 holds v9 .degree() c= w .degree()

let w be Vertex of G1; :: thesis: v9 .degree() c= b₁ .degree()

per cases ( w in the_Vertices_of G2 or w in {v} ) by A4, XBOOLE_0:def 3;

suppose w in the_Vertices_of G2 ; :: thesis: v9 .degree() c= b₁ .degree()

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:57; :: thesis: verum

end;

suppose w in {v} ; :: thesis: v9 .degree() c= b₁ .degree()

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

end;

end;

end;

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

end;

end;