let H be addAdjVertexAll of G,v,V; :: thesis: H is with_max_in_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_in_degree

consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0 .inDegree() c= v0 .inDegree() by Def13;
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 .inDegree() <> (w0 .inDegree()) +` 1 holds
w .inDegree() = w0 .inDegree()

proof

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

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

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

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

end;

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

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

end;

end;

end;

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

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

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

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

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₁ .inDegree() c= v1 .inDegree()

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

end;

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

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

end;

end;

end;

hence H is with_max_in_degree ; :: thesis: verum

end;

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

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

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

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₁ .inDegree() c= v9 .inDegree()

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

end;

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

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

end;

end;

end;

hence H is with_max_in_degree ; :: thesis: verum

end;

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

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

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

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

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₁ .inDegree() c= v9 .inDegree()

then reconsider w0 = w as Vertex of G ;

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

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

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

end;

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

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

end;

end;

end;

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

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

end;

end;

end;

hence H is with_max_in_degree ; :: thesis: verum

end;

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

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

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

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

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₁ .inDegree() c= w .inDegree()

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

end;

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

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

end;

end;

end;

hence H is with_max_in_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_in_degree

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

end;

end;