let H be addAdjVertex of G,v,e,w; :: thesis: H is with_max_in_degree

per cases ( ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) or ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) or ( not ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) & not ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) ) ) ;

suppose ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) ; :: thesis: H is with_max_in_degree

then consider G9 being addVertex of G,w such that
A10: H is addEdge of G9,v,e,w by GLIB_006:125;
thus H is with_max_in_degree by A10; :: thesis: verum

end;

suppose ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) ; :: thesis: H is with_max_in_degree

then consider G9 being addVertex of G,v such that
A11: H is addEdge of G9,v,e,w by GLIB_006:126;
thus H is with_max_in_degree by A11; :: thesis: verum

end;

suppose ( not ( v in the_Vertices_of G & not e in the_Edges_of G & not w in the_Vertices_of G ) & not ( not v in the_Vertices_of G & not e in the_Edges_of G & w in the_Vertices_of G ) ) ; :: thesis: H is with_max_in_degree

then G == H by GLIB_006:def 12;
hence H is with_max_in_degree by Th85; :: thesis: verum

end;

end;