let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V holds G1 .minDegree() c= (G2 .minDegree()) +` 2
let V be set ; :: thesis: for G1 being addLoops of G2,V holds G1 .minDegree() c= (G2 .minDegree()) +` 2
let G1 be addLoops of G2,V; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

per cases ( V c= the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose A1: V c= the_Vertices_of G2 ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

consider v2 being Vertex of G2 such that
A2: G2 .minDegree() = v2 .degree() and
A3: for w2 being Vertex of G2 holds v2 .degree() c= w2 .degree() by Th36;
A4: the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_012:def 5;
then reconsider v1 = v2 as Vertex of G1 ;

per cases ( not v2 in V or ( v2 in V & ( for w2 being Vertex of G2 st not w2 in V holds
(v2 .degree()) +` 2 c= w2 .degree() ) ) or ( v2 in V & ex w2 being Vertex of G2 st
( not w2 in V & not (v2 .degree()) +` 2 c= w2 .degree() ) ) ) ;

suppose not v2 in V ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

then A5: v1 .degree() = v2 .degree() by A1, GLIB_012:44;

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

let w1 be Vertex of G1; :: thesis: v1 .degree() c= b₁ .degree()
reconsider w2 = w1 as Vertex of G2 by A4;

per cases ( w1 in V or not w1 in V ) ;

suppose w1 in V ; :: thesis: v1 .degree() c= b₁ .degree()

then A6: w1 .degree() = (w2 .degree()) +` 2 by A1, GLIB_012:43;
A7: v1 .degree() c= w2 .degree() by A3, A5;
w2 .degree() c= w1 .degree() by A6, CARD_2:94;
hence v1 .degree() c= w1 .degree() by A7, XBOOLE_1:1; :: thesis: verum

end;

suppose not w1 in V ; :: thesis: v1 .degree() c= b₁ .degree()

then w1 .degree() = w2 .degree() by A1, GLIB_012:44;
hence v1 .degree() c= w1 .degree() by A3, A5; :: thesis: verum

end;

end;

end;

then G1 .minDegree() = v1 .degree() by Th36;
hence G1 .minDegree() c= (G2 .minDegree()) +` 2 by A2, A5, CARD_2:94; :: thesis: verum

end;

suppose A8: ( v2 in V & ( for w2 being Vertex of G2 st not w2 in V holds
(v2 .degree()) +` 2 c= w2 .degree() ) ) ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

then A9: v1 .degree() = (v2 .degree()) +` 2 by A1, GLIB_012:43;

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

let w1 be Vertex of G1; :: thesis: v1 .degree() c= b₁ .degree()
reconsider w2 = w1 as Vertex of G2 by A4;

per cases ( w1 in V or not w1 in V ) ;

suppose w1 in V ; :: thesis: v1 .degree() c= b₁ .degree()

then A10: w1 .degree() = (w2 .degree()) +` 2 by A1, GLIB_012:43;
( v2 .degree() c= w2 .degree() & 2 c= 2 ) by A3;
hence v1 .degree() c= w1 .degree() by A9, A10, CARD_2:83; :: thesis: verum

end;

suppose A11: not w1 in V ; :: thesis: v1 .degree() c= b₁ .degree()

then w1 .degree() = w2 .degree() by A1, GLIB_012:44;
hence v1 .degree() c= w1 .degree() by A8, A9, A11; :: thesis: verum

end;

end;

end;

hence G1 .minDegree() c= (G2 .minDegree()) +` 2 by A2, A9, Th36; :: thesis: verum

end;

suppose ( v2 in V & ex w2 being Vertex of G2 st
( not w2 in V & not (v2 .degree()) +` 2 c= w2 .degree() ) ) ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

then consider w2 being Vertex of G2 such that
A12: ( not w2 in V & not (v2 .degree()) +` 2 c= w2 .degree() ) ;
A13: w2 .degree() in (v2 .degree()) +` 2 by A12, ORDINAL1:16;
reconsider w1 = w2 as Vertex of G1 by A4;
A14: w1 .degree() = w2 .degree() by A1, A12, GLIB_012:44;

per cases ( for u2 being Vertex of G2 st not u2 in V holds
w2 .degree() c= u2 .degree() or ex u2 being Vertex of G2 st
( not u2 in V & not w2 .degree() c= u2 .degree() ) ) ;

suppose A15: for u2 being Vertex of G2 st not u2 in V holds
w2 .degree() c= u2 .degree() ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

now :: thesis: for u1 being Vertex of G1 holds w1 .degree() c= u1 .degree()

let u1 be Vertex of G1; :: thesis: w1 .degree() c= b₁ .degree()
reconsider u2 = u1 as Vertex of G2 by A4;

per cases ( u1 in V or not u1 in V ) ;

suppose u1 in V ; :: thesis: w1 .degree() c= b₁ .degree()

then A16: u1 .degree() = (u2 .degree()) +` 2 by A1, GLIB_012:43;
( v2 .degree() c= u2 .degree() & 2 c= 2 ) by A3;
then (v2 .degree()) +` 2 c= (u2 .degree()) +` 2 by CARD_2:83;
hence w1 .degree() c= u1 .degree() by A13, A14, A16, ORDINAL1:def 2; :: thesis: verum

end;

suppose not u1 in V ; :: thesis: w1 .degree() c= b₁ .degree()

then ( u1 .degree() = u2 .degree() & w2 .degree() c= u2 .degree() ) by A1, A15, GLIB_012:44;
hence w1 .degree() c= u1 .degree() by A14; :: thesis: verum

end;

end;

end;

then G1 .minDegree() = w1 .degree() by Th36;
hence G1 .minDegree() c= (G2 .minDegree()) +` 2 by A2, A13, A14, ORDINAL1:def 2; :: thesis: verum

end;

suppose ex u2 being Vertex of G2 st
( not u2 in V & not w2 .degree() c= u2 .degree() ) ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

then consider u2 being Vertex of G2 such that
A17: ( not u2 in V & not w2 .degree() c= u2 .degree() ) ;
( v2 .degree() c= w2 .degree() & v2 .degree() c= u2 .degree() ) by A3;
then A18: u2 .degree() = v2 .degree() by A13, A17, Lm2;
reconsider u1 = u2 as Vertex of G1 by A4;
A19: u1 .degree() = u2 .degree() by A1, A17, GLIB_012:44;

now :: thesis: for x1 being Vertex of G1 holds u1 .degree() c= x1 .degree()

let x1 be Vertex of G1; :: thesis: u1 .degree() c= b₁ .degree()
reconsider x2 = x1 as Vertex of G2 by A4;
A20: u1 .degree() c= x2 .degree() by A3, A18, A19;

per cases ( x1 in V or not x1 in V ) ;

suppose x1 in V ; :: thesis: u1 .degree() c= b₁ .degree()

then x1 .degree() = (x2 .degree()) +` 2 by A1, GLIB_012:43;
then x2 .degree() c= x1 .degree() by CARD_2:94;
hence u1 .degree() c= x1 .degree() by A20, XBOOLE_1:1; :: thesis: verum

end;

suppose not x1 in V ; :: thesis: u1 .degree() c= b₁ .degree()

hence u1 .degree() c= x1 .degree() by A1, A20, GLIB_012:44; :: thesis: verum

end;

end;

end;

then A21: G1 .minDegree() = u1 .degree() by Th36;
u1 .degree() in w2 .degree() by A17, A19, ORDINAL1:16;
hence G1 .minDegree() c= (G2 .minDegree()) +` 2 by A2, A13, A21; :: thesis: verum

end;

end;

end;

end;

end;

suppose not V c= the_Vertices_of G2 ; :: thesis: G1 .minDegree() c= (G2 .minDegree()) +` 2

then G1 == G2 by GLIB_012:def 5;
then G1 .minDegree() = G2 .minDegree() by Th62;
hence G1 .minDegree() c= (G2 .minDegree()) +` 2 by CARD_2:94; :: thesis: verum

end;

end;