let G be _Graph; :: thesis: for C being Component of G holds
( G .minDegree() c= C .minDegree() & G .minInDegree() c= C .minInDegree() & G .minOutDegree() c= C .minOutDegree() )
let C be Component of G; :: thesis: ( G .minDegree() c= C .minDegree() & G .minInDegree() c= C .minInDegree() & G .minOutDegree() c= C .minOutDegree() )
A1: the_Vertices_of C c= the_Vertices_of G ;
thus G .minDegree() c= C .minDegree() :: thesis: ( G .minInDegree() c= C .minInDegree() & G .minOutDegree() c= C .minOutDegree() )

proof

set A = { (v .degree()) where v is Vertex of G : verum } ;
set B = { (w .degree()) where w is Vertex of C : verum } ;
A2: { (w .degree()) where w is Vertex of C : verum } <> {}

proof

set w = the Vertex of C;
the Vertex of C .degree() in { (w .degree()) where w is Vertex of C : verum } ;
hence { (w .degree()) where w is Vertex of C : verum } <> {} ; :: thesis: verum

end;

now :: thesis: for x being object st x in { (w .degree()) where w is Vertex of C : verum } holds
x in { (v .degree()) where v is Vertex of G : verum }

let x be object ; :: thesis: ( x in { (w .degree()) where w is Vertex of C : verum } implies x in { (v .degree()) where v is Vertex of G : verum } )
assume x in { (w .degree()) where w is Vertex of C : verum } ; :: thesis: x in { (v .degree()) where v is Vertex of G : verum }
then consider w being Vertex of C such that
A3: x = w .degree() ;
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v .degree() by A3, GLIBPRE0:44;
hence x in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: verum

end;

then meet { (v .degree()) where v is Vertex of G : verum } c= meet { (w .degree()) where w is Vertex of C : verum } by A2, SETFAM_1:6, TARSKI:def 3;
then G .minDegree() c= meet { (w .degree()) where w is Vertex of C : verum } ;
hence G .minDegree() c= C .minDegree() ; :: thesis: verum

end;

thus G .minInDegree() c= C .minInDegree() :: thesis: G .minOutDegree() c= C .minOutDegree()

proof

set A = { (v .inDegree()) where v is Vertex of G : verum } ;
set B = { (w .inDegree()) where w is Vertex of C : verum } ;
A4: { (w .inDegree()) where w is Vertex of C : verum } <> {}

proof

set w = the Vertex of C;
the Vertex of C .inDegree() in { (w .inDegree()) where w is Vertex of C : verum } ;
hence { (w .inDegree()) where w is Vertex of C : verum } <> {} ; :: thesis: verum

end;

now :: thesis: for x being object st x in { (w .inDegree()) where w is Vertex of C : verum } holds
x in { (v .inDegree()) where v is Vertex of G : verum }

let x be object ; :: thesis: ( x in { (w .inDegree()) where w is Vertex of C : verum } implies x in { (v .inDegree()) where v is Vertex of G : verum } )
assume x in { (w .inDegree()) where w is Vertex of C : verum } ; :: thesis: x in { (v .inDegree()) where v is Vertex of G : verum }
then consider w being Vertex of C such that
A5: x = w .inDegree() ;
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v .inDegree() by A5, GLIBPRE0:44;
hence x in { (v .inDegree()) where v is Vertex of G : verum } ; :: thesis: verum

end;

then meet { (v .inDegree()) where v is Vertex of G : verum } c= meet { (w .inDegree()) where w is Vertex of C : verum } by A4, SETFAM_1:6, TARSKI:def 3;
then G .minInDegree() c= meet { (w .inDegree()) where w is Vertex of C : verum } ;
hence G .minInDegree() c= C .minInDegree() ; :: thesis: verum

end;

thus G .minOutDegree() c= C .minOutDegree() :: thesis: verum

proof

set A = { (v .outDegree()) where v is Vertex of G : verum } ;
set B = { (w .outDegree()) where w is Vertex of C : verum } ;
A6: { (w .outDegree()) where w is Vertex of C : verum } <> {}

proof

set w = the Vertex of C;
the Vertex of C .outDegree() in { (w .outDegree()) where w is Vertex of C : verum } ;
hence { (w .outDegree()) where w is Vertex of C : verum } <> {} ; :: thesis: verum

end;

now :: thesis: for x being object st x in { (w .outDegree()) where w is Vertex of C : verum } holds
x in { (v .outDegree()) where v is Vertex of G : verum }

let x be object ; :: thesis: ( x in { (w .outDegree()) where w is Vertex of C : verum } implies x in { (v .outDegree()) where v is Vertex of G : verum } )
assume x in { (w .outDegree()) where w is Vertex of C : verum } ; :: thesis: x in { (v .outDegree()) where v is Vertex of G : verum }
then consider w being Vertex of C such that
A7: x = w .outDegree() ;
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v .outDegree() by A7, GLIBPRE0:44;
hence x in { (v .outDegree()) where v is Vertex of G : verum } ; :: thesis: verum

end;

then meet { (v .outDegree()) where v is Vertex of G : verum } c= meet { (w .outDegree()) where w is Vertex of C : verum } by A6, SETFAM_1:6, TARSKI:def 3;
then G .minOutDegree() c= meet { (w .outDegree()) where w is Vertex of C : verum } ;
hence G .minOutDegree() c= C .minOutDegree() ; :: thesis: verum

end;