let G be _Graph; :: thesis:
assume A18: G is vertex-finite ; :: thesis:
thus G is with_max_degree :: thesis:

proof

set D = { (v .degree()) where v is Vertex of G : verum } ;
deffunc H₁( object ) -> set = (In (c₁,(the_Vertices_of G))) .degree() ;
consider f being Function such that
A19: dom f = the_Vertices_of G and
A20: for x being object st x in the_Vertices_of G holds
f . x = H₁(x) from FUNCT_1:sch 3();

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A21: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A19, A21;
y = (In (x,(the_Vertices_of G))) .degree() by A19, A20, A21
.= v .degree() by SUBSET_1:def 8 ;
hence y in { (v .degree()) where v is Vertex of G : verum } ; :: thesis:

end;

assume y in { (v .degree()) where v is Vertex of G : verum } ; :: thesis:
then consider v being Vertex of G such that
A22: y = v .degree() ;
y = (In (v,(the_Vertices_of G))) .degree() by A22, SUBSET_1:def 8
.= f . v by A20 ;
hence y in rng f by A19, FUNCT_1:3; :: thesis:

end;

then rng f = { (v .degree()) where v is Vertex of G : verum } by TARSKI:2;
then A23: { (v .degree()) where v is Vertex of G : verum } is finite by A18, A19, FINSET_1:8;

now :: thesis:

let x, y be set ; :: thesis:
assume A24: ( x in { (v .degree()) where v is Vertex of G : verum } & y in { (v .degree()) where v is Vertex of G : verum } ) ; :: thesis:
then consider v being Vertex of G such that
A25: x = v .degree() ;
consider w being Vertex of G such that
A26: y = w .degree() by A24;
thus x,y are_c=-comparable by A25, A26, ORDINAL1:15; :: thesis:

end;

then A27: ( { (v .degree()) where v is Vertex of G : verum } is finite & { (v .degree()) where v is Vertex of G : verum } is c=-linear ) by A23, ORDINAL1:def 8;
then A28: ( InclPoset { (v .degree()) where v is Vertex of G : verum } is connected & InclPoset { (v .degree()) where v is Vertex of G : verum } is transitive ) ;
set B = [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } );
the Vertex of G .degree() in { (v .degree()) where v is Vertex of G : verum } ;
then A29: ( not [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } ) is empty & [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } ) is finite ) by A27;
then consider x being Element of (InclPoset { (v .degree()) where v is Vertex of G : verum } ) such that
x in [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } ) and
A30: for y being Element of (InclPoset { (v .degree()) where v is Vertex of G : verum } ) st y in [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } ) & x <> y holds
y <= x by A28, ORDERS_5:25;
A31: x in { (v .degree()) where v is Vertex of G : verum } by A29;
then consider v being Vertex of G such that
A32: x = v .degree() ;

now :: thesis:

let w be Vertex of G; :: thesis:
w .degree() in the carrier of (InclPoset { (v .degree()) where v is Vertex of G : verum } ) ;
then reconsider y = w .degree() as Element of (InclPoset { (v .degree()) where v is Vertex of G : verum } ) ;

per cases ;

suppose A33: x <> y ; :: thesis:

y in [#] (InclPoset { (v .degree()) where v is Vertex of G : verum } ) ;
then [y,x] in RelIncl { (v .degree()) where v is Vertex of G : verum } by A30, A33, ORDERS_2:def 5;
hence w .degree() c= v .degree() by A31, A32, WELLORD2:def 1; :: thesis:

end;

suppose x = y ; :: thesis:

hence w .degree() c= v .degree() by A32; :: thesis:

end;

hence G is with_max_degree ; :: thesis:

end;

thus G is with_max_in_degree :: thesis:

proof

set D = { (v .inDegree()) where v is Vertex of G : verum } ;
deffunc H₁( object ) -> set = (In (c₁,(the_Vertices_of G))) .inDegree() ;
consider f being Function such that
A34: dom f = the_Vertices_of G and
A35: for x being object st x in the_Vertices_of G holds
f . x = H₁(x) from FUNCT_1:sch 3();

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A36: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A34, A36;
y = (In (x,(the_Vertices_of G))) .inDegree() by A34, A35, A36
.= v .inDegree() by SUBSET_1:def 8 ;
hence y in { (v .inDegree()) where v is Vertex of G : verum } ; :: thesis:

end;

assume y in { (v .inDegree()) where v is Vertex of G : verum } ; :: thesis:
then consider v being Vertex of G such that
A37: y = v .inDegree() ;
y = (In (v,(the_Vertices_of G))) .inDegree() by A37, SUBSET_1:def 8
.= f . v by A35 ;
hence y in rng f by A34, FUNCT_1:3; :: thesis:

end;

then rng f = { (v .inDegree()) where v is Vertex of G : verum } by TARSKI:2;
then A38: { (v .inDegree()) where v is Vertex of G : verum } is finite by A18, A34, FINSET_1:8;

now :: thesis:

let x, y be set ; :: thesis:
assume A39: ( x in { (v .inDegree()) where v is Vertex of G : verum } & y in { (v .inDegree()) where v is Vertex of G : verum } ) ; :: thesis:
then consider v being Vertex of G such that
A40: x = v .inDegree() ;
consider w being Vertex of G such that
A41: y = w .inDegree() by A39;
thus x,y are_c=-comparable by A40, A41, ORDINAL1:15; :: thesis:

end;

then A42: ( { (v .inDegree()) where v is Vertex of G : verum } is finite & { (v .inDegree()) where v is Vertex of G : verum } is c=-linear ) by A38, ORDINAL1:def 8;
then A43: ( InclPoset { (v .inDegree()) where v is Vertex of G : verum } is connected & InclPoset { (v .inDegree()) where v is Vertex of G : verum } is transitive ) ;
set B = [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } );
the Vertex of G .inDegree() in { (v .inDegree()) where v is Vertex of G : verum } ;
then A44: ( not [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) is empty & [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) is finite ) by A42;
then consider x being Element of (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) such that
x in [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) and
A45: for y being Element of (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) st y in [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) & x <> y holds
y <= x by A43, ORDERS_5:25;
A46: x in { (v .inDegree()) where v is Vertex of G : verum } by A44;
then consider v being Vertex of G such that
A47: x = v .inDegree() ;

now :: thesis:

let w be Vertex of G; :: thesis:
w .inDegree() in the carrier of (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) ;
then reconsider y = w .inDegree() as Element of (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) ;

per cases ;

suppose A48: x <> y ; :: thesis:

y in [#] (InclPoset { (v .inDegree()) where v is Vertex of G : verum } ) ;
then [y,x] in RelIncl { (v .inDegree()) where v is Vertex of G : verum } by A45, A48, ORDERS_2:def 5;
hence w .inDegree() c= v .inDegree() by A46, A47, WELLORD2:def 1; :: thesis:

end;

suppose x = y ; :: thesis:

hence w .inDegree() c= v .inDegree() by A47; :: thesis:

end;

hence G is with_max_in_degree ; :: thesis:

end;

thus G is with_max_out_degree :: thesis:

proof

set D = { (v .outDegree()) where v is Vertex of G : verum } ;
deffunc H₁( object ) -> set = (In (c₁,(the_Vertices_of G))) .outDegree() ;
consider f being Function such that
A49: dom f = the_Vertices_of G and
A50: for x being object st x in the_Vertices_of G holds
f . x = H₁(x) from FUNCT_1:sch 3();

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A51: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A49, A51;
y = (In (x,(the_Vertices_of G))) .outDegree() by A49, A50, A51
.= v .outDegree() by SUBSET_1:def 8 ;
hence y in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis:

end;

assume y in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis:
then consider v being Vertex of G such that
A52: y = v .outDegree() ;
y = (In (v,(the_Vertices_of G))) .outDegree() by A52, SUBSET_1:def 8
.= f . v by A50 ;
hence y in rng f by A49, FUNCT_1:3; :: thesis:

end;

then rng f = { (v .outDegree()) where v is Vertex of G : verum } by TARSKI:2;
then A53: { (v .outDegree()) where v is Vertex of G : verum } is finite by A18, A49, FINSET_1:8;

now :: thesis:

let x, y be set ; :: thesis:
assume A54: ( x in { (v .outDegree()) where v is Vertex of G : verum } & y in { (v .outDegree()) where v is Vertex of G : verum } ) ; :: thesis:
then consider v being Vertex of G such that
A55: x = v .outDegree() ;
consider w being Vertex of G such that
A56: y = w .outDegree() by A54;
thus x,y are_c=-comparable by A55, A56, ORDINAL1:15; :: thesis:

end;

then A57: ( { (v .outDegree()) where v is Vertex of G : verum } is finite & { (v .outDegree()) where v is Vertex of G : verum } is c=-linear ) by A53, ORDINAL1:def 8;
then A58: ( InclPoset { (v .outDegree()) where v is Vertex of G : verum } is connected & InclPoset { (v .outDegree()) where v is Vertex of G : verum } is transitive ) ;
set B = [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } );
the Vertex of G .outDegree() in { (v .outDegree()) where v is Vertex of G : verum } ;
then A59: ( not [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) is empty & [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) is finite ) by A57;
then consider x being Element of (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) such that
x in [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) and
A60: for y being Element of (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) st y in [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) & x <> y holds
y <= x by A58, ORDERS_5:25;
A61: x in { (v .outDegree()) where v is Vertex of G : verum } by A59;
then consider v being Vertex of G such that
A62: x = v .outDegree() ;

now :: thesis:

let w be Vertex of G; :: thesis:
w .outDegree() in the carrier of (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) ;
then reconsider y = w .outDegree() as Element of (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) ;

per cases ;

suppose A63: x <> y ; :: thesis:

y in [#] (InclPoset { (v .outDegree()) where v is Vertex of G : verum } ) ;
then [y,x] in RelIncl { (v .outDegree()) where v is Vertex of G : verum } by A60, A63, ORDERS_2:def 5;
hence w .outDegree() c= v .outDegree() by A61, A62, WELLORD2:def 1; :: thesis:

end;

suppose x = y ; :: thesis:

hence w .outDegree() c= v .outDegree() by A62; :: thesis:

end;

hence G is with_max_out_degree ; :: thesis:

end;