let c be Cardinal; :: thesis: for G being _trivial c -edge _Graph holds
( G .maxInDegree() = c & G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )
let G be _trivial c -edge _Graph; :: thesis: ( G .maxInDegree() = c & G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )
set v = the Vertex of G;

now :: thesis: for w being Vertex of G holds w .inDegree() c= the Vertex of G .inDegree()

let w be Vertex of G; :: thesis: w .inDegree() c= the Vertex of G .inDegree()
( w .inDegree() = G .size() & the Vertex of G .inDegree() = G .size() ) by GLIB_000:149;
hence w .inDegree() c= the Vertex of G .inDegree() ; :: thesis: verum

end;

hence G .maxInDegree() = G .size() by Th49, GLIB_000:149
.= c by Def4 ;
:: thesis: ( G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )

now :: thesis: for w being Vertex of G holds the Vertex of G .inDegree() c= w .inDegree()

let w be Vertex of G; :: thesis: the Vertex of G .inDegree() c= w .inDegree()
( w .inDegree() = G .size() & the Vertex of G .inDegree() = G .size() ) by GLIB_000:149;
hence the Vertex of G .inDegree() c= w .inDegree() ; :: thesis: verum

end;

hence G .minInDegree() = G .size() by Th37, GLIB_000:149
.= c by Def4 ;
:: thesis: ( G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )

now :: thesis: for w being Vertex of G holds w .outDegree() c= the Vertex of G .outDegree()

let w be Vertex of G; :: thesis: w .outDegree() c= the Vertex of G .outDegree()
( w .outDegree() = G .size() & the Vertex of G .outDegree() = G .size() ) by GLIB_000:149;
hence w .outDegree() c= the Vertex of G .outDegree() ; :: thesis: verum

end;

hence G .maxOutDegree() = G .size() by Th50, GLIB_000:149
.= c by Def4 ;
:: thesis: ( G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )

now :: thesis: for w being Vertex of G holds the Vertex of G .outDegree() c= w .outDegree()

let w be Vertex of G; :: thesis: the Vertex of G .outDegree() c= w .outDegree()
( w .outDegree() = G .size() & the Vertex of G .outDegree() = G .size() ) by GLIB_000:149;
hence the Vertex of G .outDegree() c= w .outDegree() ; :: thesis: verum

end;

hence G .minOutDegree() = G .size() by Th38, GLIB_000:149
.= c by Def4 ;
:: thesis: ( G .maxDegree() = c +` c & G .minDegree() = c +` c )

now :: thesis: for w being Vertex of G holds w .degree() c= the Vertex of G .degree()

let w be Vertex of G; :: thesis: w .degree() c= the Vertex of G .degree()
( w .degree() = (G .size()) +` (G .size()) & the Vertex of G .degree() = (G .size()) +` (G .size()) ) by GLIB_000:149;
hence w .degree() c= the Vertex of G .degree() ; :: thesis: verum

end;

hence G .maxDegree() = (G .size()) +` (G .size()) by Th48, GLIB_000:149
.= (G .size()) +` c by Def4
.= c +` c by Def4 ;
:: thesis: G .minDegree() = c +` c

now :: thesis: for w being Vertex of G holds the Vertex of G .degree() c= w .degree()

let w be Vertex of G; :: thesis: the Vertex of G .degree() c= w .degree()
( w .degree() = (G .size()) +` (G .size()) & the Vertex of G .degree() = (G .size()) +` (G .size()) ) by GLIB_000:149;
hence the Vertex of G .degree() c= w .degree() ; :: thesis: verum

end;

hence G .minDegree() = (G .size()) +` (G .size()) by Th36, GLIB_000:149
.= (G .size()) +` c by Def4
.= c +` c by Def4 ;
:: thesis: verum