let H be addAdjVertexAll of G,v,V; :: thesis: H is with_max_degree

per cases ( ( not v in the_Vertices_of G & V c= the_Vertices_of G ) or v in the_Vertices_of G or not V c= the_Vertices_of G ) ;

suppose A1: ( not v in the_Vertices_of G & V c= the_Vertices_of G ) ; :: thesis: H is with_max_degree

consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0 .degree() c= v0 .degree() by Def12;
A3: the_Vertices_of H = (the_Vertices_of G) \/ {v} by A1, GLIB_007:def 4;
then reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;
reconsider v1 = v as Vertex of H by A1, GLIB_007:50;
A4: for w being Vertex of H
for w0 being Vertex of G st w = w0 & w .degree() <> (w0 .degree()) +` 1 holds
w .degree() = w0 .degree()

proof

let w be Vertex of H; :: thesis: for w0 being Vertex of G st w = w0 & w .degree() <> (w0 .degree()) +` 1 holds
w .degree() = w0 .degree()
let w0 be Vertex of G; :: thesis: ( w = w0 & w .degree() <> (w0 .degree()) +` 1 implies w .degree() = w0 .degree() )
assume A5: w = w0 ; :: thesis: ( not w .degree() <> (w0 .degree()) +` 1 or w .degree() = w0 .degree() )
assume A6: w .degree() <> (w0 .degree()) +` 1 ; :: thesis: w .degree() = w0 .degree()
A7: w .degree() c= (w0 .degree()) +` 1 by A5, GLIBPRE0:58;
then A8: (w .degree()) +` 1 c= (w0 .degree()) +` 1 by A6, Lm1;
G is Subgraph of H by GLIB_006:57;
then ( w0 .inDegree() c= w .inDegree() & w0 .outDegree() c= w .outDegree() ) by A5, GLIB_000:78, CARD_1:11;
then A9: w0 .degree() c= w .degree() by CARD_2:83;
then (w0 .degree()) +` 1 c= (w .degree()) +` 1 by CARD_2:83;
then A10: (w .degree()) +` 1 = (w0 .degree()) +` 1 by A8, XBOOLE_0:def 10;

per cases ( w0 .degree() is infinite or w .degree() is finite ) by A7;

suppose A11: w0 .degree() is infinite ; :: thesis: w .degree() = w0 .degree()

then A12: w .degree() is infinite by A9;
then 1 c= w .degree() ;
then A13: (w .degree()) +` 1 = w .degree() by A12, CARD_2:76;
1 c= w0 .degree() by A11;
hence w .degree() = w0 .degree() by A10, A11, A13, CARD_2:76; :: thesis: verum

end;

suppose w .degree() is finite ; :: thesis: w .degree() = w0 .degree()

then reconsider m = w0 .degree() , n = w .degree() as Nat by A9;
m + 1 = m +` 1
.= n +` 1 by A10
.= n + 1 ;
hence w .degree() = w0 .degree() ; :: thesis: verum

end;

end;

end;

per cases ( (v0 .degree()) +` 1 c= v1 .degree() or ( v1 .degree() in (v0 .degree()) +` 1 & v9 .degree() = (v0 .degree()) +` 1 ) or ( v1 .degree() in (v0 .degree()) +` 1 & v9 .degree() <> (v0 .degree()) +` 1 & ( for w0 being Vertex of G
for w being Vertex of H st w0 = w & w .degree() = (w0 .degree()) +` 1 holds
(w0 .degree()) +` 1 c= v0 .degree() ) ) or ( v1 .degree() c= (v0 .degree()) +` 1 & v9 .degree() <> (v0 .degree()) +` 1 & ex w0 being Vertex of G ex w being Vertex of H st
( w0 = w & w .degree() = (w0 .degree()) +` 1 & not ( w .degree() = (w0 .degree()) +` 1 & (w0 .degree()) +` 1 c= v0 .degree() ) ) ) ) by ORDINAL1:16;

suppose A14: (v0 .degree()) +` 1 c= v1 .degree() ; :: thesis: H is with_max_degree

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

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

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

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

then reconsider w0 = w as Vertex of G ;
A15: w .degree() c= (w0 .degree()) +` 1 by GLIBPRE0:58;
( w0 .degree() c= v0 .degree() & 1 c= 1 ) by A2;
then (w0 .degree()) +` 1 c= (v0 .degree()) +` 1 by CARD_2:83;
then w .degree() c= (v0 .degree()) +` 1 by A15, XBOOLE_1:1;
hence w .degree() c= v1 .degree() by A14, XBOOLE_1:1; :: thesis: verum

end;

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

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

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

suppose A16: ( v1 .degree() in (v0 .degree()) +` 1 & v9 .degree() = (v0 .degree()) +` 1 ) ; :: thesis: H is with_max_degree

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

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

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

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

then reconsider w0 = w as Vertex of G ;
A17: w .degree() c= (w0 .degree()) +` 1 by GLIBPRE0:58;
( w0 .degree() c= v0 .degree() & 1 c= 1 ) by A2;
then (w0 .degree()) +` 1 c= (v0 .degree()) +` 1 by CARD_2:83;
hence w .degree() c= v9 .degree() by A16, A17, XBOOLE_1:1; :: thesis: verum

end;

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

then w = v1 by TARSKI:def 1;
hence w .degree() c= v9 .degree() by A16, ORDINAL1:def 2; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

suppose A18: ( v1 .degree() in (v0 .degree()) +` 1 & v9 .degree() <> (v0 .degree()) +` 1 & ( for w0 being Vertex of G
for w being Vertex of H st w0 = w & w .degree() = (w0 .degree()) +` 1 holds
(w0 .degree()) +` 1 c= v0 .degree() ) ) ; :: thesis: H is with_max_degree

then A19: v9 .degree() = v0 .degree() by A4;

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

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

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

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

then reconsider w0 = w as Vertex of G ;

per cases ( w .degree() = (w0 .degree()) +` 1 or w .degree() <> (w0 .degree()) +` 1 ) ;

suppose w .degree() = (w0 .degree()) +` 1 ; :: thesis: b₁ .degree() c= v9 .degree()

hence w .degree() c= v9 .degree() by A18, A19; :: thesis: verum

end;

suppose w .degree() <> (w0 .degree()) +` 1 ; :: thesis: b₁ .degree() c= v9 .degree()

then w .degree() = w0 .degree() by A4;
hence w .degree() c= v9 .degree() by A2, A19; :: thesis: verum

end;

end;

end;

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

then w = v1 by TARSKI:def 1;
hence w .degree() c= v9 .degree() by A18, A19, Lm7; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

suppose A20: ( v1 .degree() c= (v0 .degree()) +` 1 & v9 .degree() <> (v0 .degree()) +` 1 & ex w0 being Vertex of G ex w being Vertex of H st
( w0 = w & w .degree() = (w0 .degree()) +` 1 & not ( w .degree() = (w0 .degree()) +` 1 & (w0 .degree()) +` 1 c= v0 .degree() ) ) ) ; :: thesis: H is with_max_degree

consider w0 being Vertex of G, w being Vertex of H such that
A21: ( w0 = w & w .degree() = (w0 .degree()) +` 1 ) and
A22: not (w0 .degree()) +` 1 c= v0 .degree() by A20;
v0 .degree() in w .degree() by A21, A22, ORDINAL1:16;
then ( v0 .degree() c= w .degree() & v0 .degree() <> w .degree() ) by ORDINAL1:16;
then A23: (v0 .degree()) +` 1 c= w .degree() by Lm1;

now :: thesis: for u being Vertex of H holds u .degree() c= w .degree()

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

per cases ( u in the_Vertices_of G or u in {v} ) by A3, XBOOLE_0:def 3;

suppose u in the_Vertices_of G ; :: thesis: b₁ .degree() c= w .degree()

then reconsider u0 = u as Vertex of G ;
A24: u .degree() c= (u0 .degree()) +` 1 by GLIBPRE0:58;
( u0 .degree() c= v0 .degree() & 1 c= 1 ) by A2;
then (u0 .degree()) +` 1 c= (v0 .degree()) +` 1 by CARD_2:83;
then (u0 .degree()) +` 1 c= w .degree() by A23, XBOOLE_1:1;
hence u .degree() c= w .degree() by A24, XBOOLE_1:1; :: thesis: verum

end;

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

then u = v1 by TARSKI:def 1;
hence u .degree() c= w .degree() by A20, A23, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence H is with_max_degree ; :: thesis: verum

end;

end;

end;

suppose ( v in the_Vertices_of G or not V c= the_Vertices_of G ) ; :: thesis: H is with_max_degree

then G == H by GLIB_007:def 4;
hence H is with_max_degree by Th85; :: thesis: verum

end;

end;