now :: thesis: for d being set st d in { (v .degree()) where v is Vertex of G : verum } holds
d c= (G .size()) +` (G .size())

let d be set ; :: thesis: ( d in { (v .degree()) where v is Vertex of G : verum } implies d c= (G .size()) +` (G .size()) )
assume d in { (v .degree()) where v is Vertex of G : verum } ; :: thesis: d c= (G .size()) +` (G .size())
then consider v being Vertex of G such that
A1: d = v .degree() ;
( card (v .edgesIn()) c= card (the_Edges_of G) & card (v .edgesOut()) c= card (the_Edges_of G) ) by CARD_1:11;
hence d c= (G .size()) +` (G .size()) by A1, CARD_2:83; :: thesis: verum

end;

then G .supDegree() c= (G .size()) +` (G .size()) by ZFMISC_1:76;
hence G .supDegree() is natural ; :: thesis: verum