let G be _Graph; :: thesis: ( G is vertex-finite implies ( G is with_max_degree & G is with_max_in_degree & G is with_max_out_degree ) )
assume A18: G is vertex-finite ; :: thesis: ( G is with_max_degree & G is with_max_in_degree & G is with_max_out_degree )
thus G is with_max_degree :: thesis: ( G is with_max_in_degree & G is with_max_out_degree )

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: for y being object holds
( ( y in rng f implies y in { (v .degree()) where v is Vertex of G : verum } ) & ( y in { (v .degree()) where v is Vertex of G : verum } implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in { (v .degree()) where v is Vertex of G : verum } ) & ( y in { (v .degree()) where v is Vertex of G : verum } implies y in rng f ) )

hereby :: thesis: ( y in { (v .degree()) where v is Vertex of G : verum } implies y in rng f )

assume y in rng f ; :: thesis: y in { (v .degree()) where v is Vertex of G : verum }
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: verum

end;

assume y in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: y in rng f
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: verum

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: for x, y being set st x in { (v .degree()) where v is Vertex of G : verum } & y in { (v .degree()) where v is Vertex of G : verum } holds
x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in { (v .degree()) where v is Vertex of G : verum } & y in { (v .degree()) where v is Vertex of G : verum } implies x,y are_c=-comparable )
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: x,y are_c=-comparable
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: verum

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: for w being Vertex of G holds w .degree() c= v .degree()

let w be Vertex of G; :: thesis: b₁ .degree() c= v .degree()
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 ( x <> y or x = y ) ;

suppose A33: x <> y ; :: thesis: b₁ .degree() c= v .degree()

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: verum

end;

suppose x = y ; :: thesis: b₁ .degree() c= v .degree()

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

end;

end;

end;

hence G is with_max_degree ; :: thesis: verum

end;

thus G is with_max_in_degree :: thesis: G is with_max_out_degree

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: for y being object holds
( ( y in rng f implies y in { (v .inDegree()) where v is Vertex of G : verum } ) & ( y in { (v .inDegree()) where v is Vertex of G : verum } implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in { (v .inDegree()) where v is Vertex of G : verum } ) & ( y in { (v .inDegree()) where v is Vertex of G : verum } implies y in rng f ) )

hereby :: thesis: ( y in { (v .inDegree()) where v is Vertex of G : verum } implies y in rng f )

assume y in rng f ; :: thesis: y in { (v .inDegree()) where v is Vertex of G : verum }
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: verum

end;

assume y in { (v .inDegree()) where v is Vertex of G : verum } ; :: thesis: y in rng f
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: verum

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: for x, y being set st x in { (v .inDegree()) where v is Vertex of G : verum } & y in { (v .inDegree()) where v is Vertex of G : verum } holds
x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in { (v .inDegree()) where v is Vertex of G : verum } & y in { (v .inDegree()) where v is Vertex of G : verum } implies x,y are_c=-comparable )
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: x,y are_c=-comparable
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: verum

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: for w being Vertex of G holds w .inDegree() c= v .inDegree()

let w be Vertex of G; :: thesis: b₁ .inDegree() c= v .inDegree()
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 ( x <> y or x = y ) ;

suppose A48: x <> y ; :: thesis: b₁ .inDegree() c= v .inDegree()

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: verum

end;

suppose x = y ; :: thesis: b₁ .inDegree() c= v .inDegree()

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

end;

end;

end;

hence G is with_max_in_degree ; :: thesis: verum

end;

thus G is with_max_out_degree :: thesis: verum

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: for y being object holds
( ( y in rng f implies y in { (v .outDegree()) where v is Vertex of G : verum } ) & ( y in { (v .outDegree()) where v is Vertex of G : verum } implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in { (v .outDegree()) where v is Vertex of G : verum } ) & ( y in { (v .outDegree()) where v is Vertex of G : verum } implies y in rng f ) )

hereby :: thesis: ( y in { (v .outDegree()) where v is Vertex of G : verum } implies y in rng f )

assume y in rng f ; :: thesis: y in { (v .outDegree()) where v is Vertex of G : verum }
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: verum

end;

assume y in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: y in rng f
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: verum

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: for x, y being set st x in { (v .outDegree()) where v is Vertex of G : verum } & y in { (v .outDegree()) where v is Vertex of G : verum } holds
x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in { (v .outDegree()) where v is Vertex of G : verum } & y in { (v .outDegree()) where v is Vertex of G : verum } implies x,y are_c=-comparable )
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: x,y are_c=-comparable
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: verum

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: for w being Vertex of G holds w .outDegree() c= v .outDegree()

let w be Vertex of G; :: thesis: b₁ .outDegree() c= v .outDegree()
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 ( x <> y or x = y ) ;

suppose A63: x <> y ; :: thesis: b₁ .outDegree() c= v .outDegree()

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: verum

end;

suppose x = y ; :: thesis: b₁ .outDegree() c= v .outDegree()

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

end;

end;

end;

hence G is with_max_out_degree ; :: thesis: verum

end;