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 GLIBPRE0:27;
hence w .inDegree() c= the Vertex of G .inDegree() ; :: thesis: verum
end;
hence G .maxInDegree() = G .size() by Th49, GLIBPRE0:27
.= 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 GLIBPRE0:27;
hence the Vertex of G .inDegree() c= w .inDegree() ; :: thesis: verum
end;
hence G .minInDegree() = G .size() by Th37, GLIBPRE0:27
.= 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 GLIBPRE0:27;
hence w .outDegree() c= the Vertex of G .outDegree() ; :: thesis: verum
end;
hence G .maxOutDegree() = G .size() by Th50, GLIBPRE0:27
.= 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 GLIBPRE0:27;
hence the Vertex of G .outDegree() c= w .outDegree() ; :: thesis: verum
end;
hence G .minOutDegree() = G .size() by Th38, GLIBPRE0:27
.= 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 GLIBPRE0:27;
hence w .degree() c= the Vertex of G .degree() ; :: thesis: verum
end;
hence G .maxDegree() = (G .size()) +` (G .size()) by Th48, GLIBPRE0:27
.= (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 GLIBPRE0:27;
hence the Vertex of G .degree() c= w .degree() ; :: thesis: verum
end;
hence G .minDegree() = (G .size()) +` (G .size()) by Th36, GLIBPRE0:27
.= (G .size()) +` c by Def4
.= c +` c by Def4 ;
:: thesis: verum